Basic.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

36 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic Progressions

Main definitions:

Set.IsAPOfLengthWith (s : Set α) (l : ℕ∞) (a d : α) : predicate asserting that s is the set consisting of an arithmetic progression of length l (possibly infinite) with first term a and difference d. Useful for cases in which additional conditions need to be applied to the individual terms and/or difference.
Set.IsAPOfLength (s : Set α) (l : ℕ∞) : predicate asserting that s is the set consisting of an arithmetic progression of length l, for some some first term and difference.

Imports (4)

Imported by 2 files

def Set.IsAPOfLengthWith Documented declaration: IsAPOfLengthWith line 44 source
Source documentation
A set $S$ is an arithmetic progression of length $l$ with first term $a$ and difference $d$ if $S = \{a, a + d, ..., a + (l - 1)d\}$, if $l$ if finite, else $S = {a, a + d, a + 2d, ...}. This can be written as s.IsAPOfLengthWith l a d, where l : ℕ∞ may take the infinite value ⊤.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat
Proof uses: And, Eq, ENat.card, Set.ofPred, Exists, Nat, LT.lt, HAdd.hAdd, HSMul.hSMul
12 instances, coercions and auxiliary constants left out.
```
def Set.IsAPOfLengthWith (s : Set α) (l : ℕ∞) (a d : α) : Prop :=
…
```
def List.IsAPOfLengthWith A list version of Set.IsAPOfLengthWith line 51 source
Source documentation
A list version of Set.IsAPOfLengthWith. Useful when order preservation is required, for example when considering images under arbitrary functions.

no axioms what this means
Statement uses: AddCommMonoid, List, Nat
Proof uses: Or, Eq, List.map, HAdd.hAdd, HSMul.hSMul, List.range, List.reverse
8 instances, coercions and auxiliary constants left out.
```
def List.IsAPOfLengthWith (s : List α) (l : ℕ) (a d : α) : Prop :=
…
```
theorem Set.IsAPOfLengthWith.card line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat, Set.IsAPOfLengthWith, Eq, ENat.card
Proof uses: And.left, Set.ofPred, Exists, Nat, LT.lt, HAdd.hAdd, HSMul.hSMul
13 instances, coercions and auxiliary constants left out.
theorem Set.IsAPOfLengthWith.eq line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat, Set.IsAPOfLengthWith, Eq, Set.ofPred, Exists, Nat, LT.lt, HAdd.hAdd, HSMul.hSMul
Proof uses: And.right, ENat.card
23 instances, coercions and auxiliary constants left out.
theorem Set.IsAPOfLengthWith.zero An arithmetic progression with first term a and difference d is of length zero if and only if s is empty line 64 source
Source documentation
An arithmetic progression with first term a and difference d is of length zero if and only if s is empty.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Iff, Set.IsAPOfLengthWith, OfNat.ofNat, ENat, Eq, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, ENat.card, Set.ofPred, Exists, Nat, LT.lt, HAdd.hAdd, HSMul.hSMul, congr, False, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl and 2 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem zero : s.IsAPOfLengthWith 0 a d ↔ s = ∅ := by simp [IsAPOfLengthWith]
…
```
Mentions: Set.IsAPOfLengthWith
theorem Set.IsAPOfLengthWith.one An arithmetic progression with first term a and difference d is of length one if and only if s is a singleton line 69 source
Source documentation
An arithmetic progression with first term a and difference d is of length one if and only if s is a singleton.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Iff, Set.IsAPOfLengthWith, OfNat.ofNat, ENat, Eq, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, Set.encard, True, And, congrFun', congrArg, Set.ofPred, Exists, Nat, LT.lt, HAdd.hAdd, HSMul.hSMul, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, zero_nsmul, add_zero and 5 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem one : s.IsAPOfLengthWith 1 a d ↔ s = {a} := by simp +contextual [IsAPOfLengthWith]
…
```
Mentions: Set.IsAPOfLengthWith
theorem List.IsAPOfLengthWith.length line 77 source
standard axioms: propext what this means
Statement uses: AddCommMonoid, List, Nat, List.IsAPOfLengthWith, Eq, List.length
Proof uses: List.map, HAdd.hAdd, HSMul.hSMul, List.range, List.reverse, Or, Or.inl, of_eq_true, Eq.trans, True, congrFun', congrArg, List.length_map, List.length_range, eq_self, Or.inr, id, Eq.mp, List.map_reverse, List.length_reverse and 1 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem List.IsAPOfLengthWith.zero An arithmetic progression with first term a and difference d is of length zero if and only if s is empty line 83 source
Source documentation
An arithmetic progression with first term a and difference d is of length zero if and only if s is empty.

standard axioms: propext what this means
Statement uses: AddCommMonoid, List, Iff, List.IsAPOfLengthWith, OfNat.ofNat, Nat, Eq, List.nil
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Or, List.map, HAdd.hAdd, HSMul.hSMul, List.range, List.reverse, congr, List.map_nil, or_self, iff_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem zero : s.IsAPOfLengthWith 0 a d ↔ s = [] := by
…
```
theorem List.IsAPOfLengthWith.one An arithmetic progression with first term a and difference d is of length one if and only if s is a singleton line 89 source
Source documentation
An arithmetic progression with first term a and difference d is of length one if and only if s is a singleton.

standard axioms: propext what this means
Statement uses: AddCommMonoid, List, Iff, List.IsAPOfLengthWith, OfNat.ofNat, Nat, Eq, List.cons, List.nil
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Or, List.map, HAdd.hAdd, HSMul.hSMul, List.range, List.reverse, congr, List.map_cons, zero_nsmul, add_zero, List.map_nil, List.reverse_cons, or_self, iff_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem one : s.IsAPOfLengthWith 1 a d ↔ s = [a] := by
…
```
theorem Set.isAPOfLengthWith_pair In an abelian additive group α, the set {a, b} with a ≠ b is an arithmetic progression of length 2 with first term a and difference b - a line 96 source
Source documentation
In an abelian additive group α, the set {a, b} with a ≠ b is an arithmetic progression of length 2 with first term a and difference b - a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, AddCommGroup, Ne, Set.IsAPOfLengthWith, Insert.insert, Set, Singleton.singleton, OfNat.ofNat, ENat, Nat, HSub.hSub
Proof uses: Eq.mpr, And, Eq, Finset.card, Finset, Set.ofPred, Exists, LE.le, HAdd.hAdd, HSMul.hSMul, id, congr, ENat.card, LT.lt, congrArg, congrFun', Eq.trans, Fintype.card, ENat.card_eq_coe_fintype_card, Fintype.ofFinset and 43 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem Set.isAPOfLengthWith_pair {α : Type*} [DecidableEq α] [AddCommGroup α]
    {a b : α} (hab : a ≠ b) :
    Set.IsAPOfLengthWith {a, b} 2 a (b - a) := by
…
```
Mentions: Set.IsAPOfLengthWith
theorem Nat.isAPOfLengthWith_pair The set {a, b} : Set ℕ with a < b is an arithmetic progression of length 2 with first term a and difference b - a line 111 source
Source documentation
The set {a, b} : Set ℕ with a < b is an arithmetic progression of length 2 with first term a and difference b - a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Set.IsAPOfLengthWith, Insert.insert, Set, Singleton.singleton, OfNat.ofNat, ENat, HSub.hSub
Proof uses: Exists, Eq, HAdd.hAdd, Nat.exists_eq_add_of_lt, Eq.mpr, Set.ofPred, And, LE.le, HMul.hMul, id, Eq.trans, ENat.card, HSMul.hSMul, True, congr, congrArg, congrFun', Fintype.card, add_assoc, ENat.card_eq_coe_fintype_card and 40 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem Nat.isAPOfLengthWith_pair {a b : ℕ} (hab : a < b) :
    Set.IsAPOfLengthWith {a, b} 2 a (b - a) := by
…
```
Mentions: Set.IsAPOfLengthWith
def Set.IsAPOfLength The predicate that a set s is an arithmetic progression of length l (possibly infinite) line 122 source
Source documentation
The predicate that a set s is an arithmetic progression of length l (possibly infinite). This predicate does not assert a specific value for the first term or the difference of the arithmetic progression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat
Proof uses: Exists, Set.IsAPOfLengthWith
```
def Set.IsAPOfLength (s : Set α) (l : ℕ∞) : Prop :=
…
```
def List.IsAPOfLength A list version of Set.IsAPOfLength line 129 source
Source documentation
A list version of Set.IsAPOfLength. Useful when order preservation is required, for example when considering images under arbitrary functions.

no axioms what this means
Statement uses: AddCommMonoid, List, Nat
Proof uses: Exists, List.IsAPOfLengthWith
```
def List.IsAPOfLength (s : List α) (l : ℕ) : Prop :=
…
```
theorem Set.IsAPOfLength.card line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat, Set.IsAPOfLength, Eq, ENat.card
Proof uses: And.left, Set.ofPred, Exists, Nat, LT.lt, HAdd.hAdd, Exists.choose, Set.IsAPOfLengthWith, HSMul.hSMul, Exists.choose_spec
13 instances, coercions and auxiliary constants left out.
theorem Set.IsAPOfLength.eq line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat, Set.IsAPOfLength, Exists, Eq, Set.ofPred, Nat, LT.lt, HAdd.hAdd, HSMul.hSMul
Proof uses: Exists.intro, Exists.choose, Set.IsAPOfLengthWith, Exists.choose_spec, And.right, ENat.card
23 instances, coercions and auxiliary constants left out.
theorem Set.IsAPOfLength.zero Only the empty set is a finite arithmetic progression of length $0$ line 144 source
Source documentation
Only the empty set is a finite arithmetic progression of length $0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Iff, Set.IsAPOfLength, OfNat.ofNat, ENat, Eq, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Exists, Set.IsAPOfLengthWith, funext, iff_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
@[simp] theorem zero : s.IsAPOfLength 0 ↔ s = ∅ := by simp [Set.IsAPOfLength]
```
Mentions: Set.IsAPOfLength
theorem Set.IsAPOfLength.one Only singletons are finite arithmetic progressions of length $1$ line 147 source
Source documentation
Only singletons are finite arithmetic progressions of length $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Iff, Set.IsAPOfLength, OfNat.ofNat, ENat, Exists, Eq, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.IsAPOfLengthWith, funext, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
@[simp] theorem one : s.IsAPOfLength 1 ↔ ∃ a, s = {a} := by simp [IsAPOfLength]
```
Mentions: Set.IsAPOfLength
theorem Set.IsAPOfLength.congr If a set is an arithmetic progression of lengths l₁ and l₂, then the lengths are equal line 151 source
Source documentation
If a set is an arithmetic progression of lengths l₁ and l₂, then the lengths are equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat, Set.IsAPOfLength, Eq
Proof uses: Eq.mpr, ENat.card, id, congrArg, Eq.symm, Set.IsAPOfLength.card, Eq.refl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem congr {s : Set α} {l₁ l₂ : ℕ∞}
    (h₁ : s.IsAPOfLength l₁) (h₂ : s.IsAPOfLength l₂) :
    l₁ = l₂ := by
…
```
theorem List.IsAPOfLength.length line 164 source
standard axioms: propext what this means
Statement uses: AddCommMonoid, List, Nat, List.IsAPOfLength, Eq, List.length
Proof uses: Exists, List.IsAPOfLengthWith, List.IsAPOfLengthWith.length
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem List.IsAPOfLength.zero Only the empty list is a finite arithmetic progression of length $0$ line 169 source
Source documentation
Only the empty list is a finite arithmetic progression of length $0$.

standard axioms: Quot.sound, propext what this means
Statement uses: AddCommMonoid, List, Iff, List.IsAPOfLength, OfNat.ofNat, Nat, Eq, List.nil
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Exists, List.IsAPOfLengthWith, funext, iff_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
@[simp] theorem zero : s.IsAPOfLength 0 ↔ s = [] := by simp [IsAPOfLength]
```
Mentions: List.IsAPOfLength
theorem List.IsAPOfLength.one Only singletons are finite arithmetic progressions of length $1$ line 172 source
Source documentation
Only singletons are finite arithmetic progressions of length $1$.

standard axioms: Quot.sound, propext what this means
Statement uses: AddCommMonoid, List, Iff, List.IsAPOfLength, OfNat.ofNat, Nat, Exists, Eq, List.cons, List.nil
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List.IsAPOfLengthWith, funext, iff_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
@[simp] theorem one : s.IsAPOfLength 1 ↔ ∃ a, s = [a] := by simp [IsAPOfLength]
```
Mentions: List.IsAPOfLength
theorem List.IsAPOfLength.congr If a list is an arithmetic progression of lengths l₁ and l₂, then the lengths are equal line 176 source
Source documentation
If a list is an arithmetic progression of lengths l₁ and l₂, then the lengths are equal.

standard axioms: propext what this means
Statement uses: AddCommMonoid, List, Nat, List.IsAPOfLength, Eq
Proof uses: Eq.mpr, List.length, id, congrArg, Eq.symm, List.IsAPOfLength.length, Eq.refl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem congr {s : List α} {l₁ l₂ : ℕ}
    (h₁ : s.IsAPOfLength l₁) (h₂ : s.IsAPOfLength l₂) :
    l₁ = l₂ := by
…
```
theorem Set.isAPOfLength_pair line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, AddCommGroup, Ne, Set.IsAPOfLength, Insert.insert, Set, Singleton.singleton, OfNat.ofNat, ENat, Nat
Proof uses: Exists.intro, Exists, Set.IsAPOfLengthWith, HSub.hSub, Set.isAPOfLengthWith_pair
20 instances, coercions and auxiliary constants left out.
theorem Nat.isAPOfLength_pair line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Set.IsAPOfLength, Insert.insert, Set, Singleton.singleton, OfNat.ofNat, ENat
Proof uses: Exists.intro, Exists, Set.IsAPOfLengthWith, HSub.hSub, Nat.isAPOfLengthWith_pair
20 instances, coercions and auxiliary constants left out.
theorem Set.not_isAPOfLength_empty The empty set is not an arithmetic progression of positive length line 192 source
Source documentation
The empty set is not an arithmetic progression of positive length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, ENat, LT.lt, OfNat.ofNat, Not, Set.IsAPOfLength, EmptyCollection.emptyCollection, Set
Proof uses: False.elim, False, Eq.mp, Eq.trans, congrArg, Set.IsAPOfLength.congr, Iff.mpr, Eq, Set.IsAPOfLength.zero, rfl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Set.not_isAPOfLength_empty {l : ℕ∞} (hl : 0 < l) :
    ¬Set.IsAPOfLength (∅ : Set α) l :=
…
```
Mentions: Set.IsAPOfLength
def Set.IsAPOfLengthFree We say that a set s is free of arithmetic progressions of length l if s contains no non-trivial arithmetic progressions of length l line 198 source
Source documentation
We say that a set s is free of arithmetic progressions of length l if s contains no non-trivial arithmetic progressions of length l. Written as Set.IsAPOfLengthFree s l. -

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat
Proof uses: LE.le, Set.IsAPOfLength, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def Set.IsAPOfLengthFree (s : Set α) (l : ℕ∞) : Prop :=
…
```
theorem Set.isAPOfLengthFree_one Any set is free of arithmetic progressions of length 1, because such APs are all trivial line 202 source
Source documentation
Any set is free of arithmetic progressions of length 1, because such APs are all trivial.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Set.IsAPOfLengthFree, OfNat.ofNat, ENat
Proof uses: of_eq_true, LE.le, Set.IsAPOfLength, Eq.trans, True, forall_congr, implies_congr, Eq.refl, Exists, Eq, Singleton.singleton, implies_true
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Set.isAPOfLengthFree_one (s : Set α) : s.IsAPOfLengthFree 1 := by
…
```
theorem Set.isAPOfLengthFree_zero Any set is free of arithmetic progressions of length 0, because such APs are all trivial line 206 source
Source documentation
Any set is free of arithmetic progressions of length 0, because such APs are all trivial.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Set.IsAPOfLengthFree, OfNat.ofNat, ENat
Proof uses: of_eq_true, LE.le, Set.IsAPOfLength, Eq.trans, True, forall_congr, implies_congr, Eq.refl, Eq, EmptyCollection.emptyCollection, implies_true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Set.isAPOfLengthFree_zero (s : Set α) : s.IsAPOfLengthFree 0 := by
…
```
theorem Set.IsAPOfLength.not_isAPOfLengthFree Any non-trivial arithmetic progression cannot be free of arithmetic progressions line 210 source
Source documentation
Any non-trivial arithmetic progression cannot be free of arithmetic progressions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, ENat, Set.IsAPOfLength, LT.lt, OfNat.ofNat, Not, Set.IsAPOfLengthFree
Proof uses: Eq.mpr, Exists, And, LE.le, id, Eq, Eq.trans, congrArg, funext, Exists.intro, And.intro, le_rfl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Set.IsAPOfLength.not_isAPOfLengthFree {s : Set α} {l : ℕ∞}
    (hs : s.IsAPOfLength l) (hl : 1 < l) : ¬s.IsAPOfLengthFree l := by
…
```
def Set.IsAPOfLengthFree.maxCard Define the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression line 218 source
Source documentation
Define the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, LE.le, Finset.Icc, OfNat.ofNat, Set.IsAPOfLengthFree, ENat, Eq, Finset.card
12 instances, coercions and auxiliary constants left out.
```
noncomputable def Set.IsAPOfLengthFree.maxCard (k : ℕ) (N : ℕ) : ℕ :=
…
```
theorem Set.IsAPOfLengthFree.maxCard_zero line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set.IsAPOfLengthFree.maxCard, OfNat.ofNat
Proof uses: Eq.mpr, SupSet.sSup, Set.ofPred, Exists, Finset, And, LE.le, Finset.Icc, Finset.card, id, congrFun', congrArg, Set, Set.IsAPOfLengthFree, ENat, funext, Eq.trans, propext, exists_prop_congr, Iff.of_eq and 12 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Set.IsAPOfLengthFree.maxCard_one line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set.IsAPOfLengthFree.maxCard, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Set.IsAPOfLengthFree.maxCard_zero, of_eq_true, Eq.trans, SupSet.sSup, Set.ofPred, Exists, Finset, And, LE.le, Finset.Icc, Finset.card, True, congr, Set, Set.IsAPOfLengthFree, ENat and 8 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Set.ContainsAP A set A contains an arithmetic progression of length k with difference d line 233 source
Source documentation
A set A contains an arithmetic progression of length k with difference d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, Nat
Proof uses: Exists, And, LE.le, Set.IsAPOfLengthWith, ENat
3 instances, coercions and auxiliary constants left out.
```
def Set.ContainsAP (A : Set α) (k : ℕ) (d : α) : Prop :=
…
```
def ContainsMonoAPofLength line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Finite, Set, Nat
Proof uses: Exists, And, Set.IsAPOfLength, Set.image, Membership.mem, ENat, Eq
6 instances, coercions and auxiliary constants left out.
def HasMonotoneAP A function f : β → α has a monotone k-term arithmetic progression if there exists a choice of indices `b 1 < b 2 < line 246 source
Source documentation
A function f : β → α has a monotone k-term arithmetic progression if there exists a choice of indices b 1 < b 2 < ... < b k such that the subsequence f (b i) forms an increasing or decreasing arithmetic progression of length k.

no axioms what this means
Statement uses: AddCommMonoid, Preorder, Nat
Proof uses: Exists, List, And, List.IsAPOfLength, List.map, List.Pairwise, LT.lt
1 instances, coercions and auxiliary constants left out.
```
def HasMonotoneAP {β : Type*} [Preorder β] (f : β → α) (k : ℕ) : Prop :=
…
```
def Finset.maxAPFreeCard Define the largest possible size of a subset of a finset s that does not contain any non-trivial k-term arithmetic progression line 253 source
Source documentation
Define the largest possible size of a subset of a finset s that does not contain any non-trivial k-term arithmetic progression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Finset
Proof uses: Finset.sup, Finset.filter, Set.IsAPOfLengthFree, ENat, Classical.propDecidable, Finset.powerset, Finset.card
7 instances, coercions and auxiliary constants left out.
```
noncomputable def Finset.maxAPFreeCard (k : ℕ) (s : Finset α) : ℕ :=
…
```