awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
rw : a * b * a • d = a * c * (a * c)
rw₁ : a * b * (a * d) = a * c * (a * c)
rw₂ : a * a * (b * d) = a * c * (a * c)
⊢ a • b * a • d = a * c * (a * c)
have rw₃ : a * a * (c * c) = a * c * (a * c)
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
rw : a * b * a • d = a * c * (a * c)
rw₁ : a * b * (a * d) = a * c * (a * c)
rw₂ : a * a * (b * d) = a * c * (a * c)
rw₃ : a * a * (c * c) = a * c * (a * c)
⊢ a • b * a • d = a * c * (a * c)
have rw₄ : a * c * (a * c) = a * c * (a * c)
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
s : Set ℕ
⊢ ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c
have refine_1 : ∀ (a : ℕ) (_ha : a ∈ s) (b : ℕ) (hb : b ∈ s) (c : ℕ) (hc : c ∈ s) (habc : a + c = b + b), a = b → a = c
Tactic: refine forall₄_congr fun a _ha b hb => forall₃_congr fun c hc habc => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
s : Set ℕ
refine_1 : ∀ (a : ℕ) (_ha : a ∈ s) (b : ℕ) (hb : b ∈ s) (c : ℕ) (hc : c ∈ s) (habc : a + c = b + b), a = b → a = c
⊢ ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c
have refine_2 : ∀ (a : ℕ) (_ha : a ∈ s) (b : ℕ) (hb : b ∈ s) (c : ℕ) (hc : c ∈ s) (habc : a + c = b + b), a = c → a = b
Tactic: refine forall₄_congr fun a _ha b hb => forall₃_congr fun c hc habc => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b
have habc₁ : 2 * a = 2 * b
Tactic: simp_rw [← two_mul] at habc
Cleared hypotheses: habc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s t_1 t u : Finset α
htu : t ≤ u
⊢ LE.le (α := ℕ)
    ((fun (s : Finset α) ↦ Nat.findGreatest (fun (m : ℕ) ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (↑t : Set α)) #s) t)
    ((fun (s : Finset α) ↦ Nat.findGreatest (fun (m : ℕ) ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (↑t : Set α)) #s) u)
have refine : ∀ (m : ℕ), (∃ t_2 ⊆ t, #t_2 = m ∧ ThreeGPFree (↑t_2 : Set α)) → ∃ t ⊆ u, #t = m ∧ ThreeGPFree (↑t : Set α)
Tactic: refine Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ ThreeGPFree (↑∅ : Set α)
have norm_cast : ThreeGPFree.{u_2} (α := α) ∅
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) {a} : ℕ) (1 : ℕ)
have refine : ThreeGPFree (↑{a} : Set α)
Tactic: refine ThreeGPFree.mulRothNumber_eq ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ ThreeGPFree (↑{a} : Set α)
have rw : ThreeGPFree (α := α) {a}
Tactic: rw [coe_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (s ∪ t)
hu : ThreeGPFree (↑u : Set α)
⊢ #u = #(u ∩ s ∪ u ∩ t)
have rw : #u = #(u ∩ (s ∪ t))
Tactic: rw [← inter_union_distrib_left, inter_eq_left.2 hus]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (s ∪ t)
hu : ThreeGPFree (↑u : Set α)
rw : #u = #(u ∩ (s ∪ t))
⊢ #u = #(u ∩ s ∪ u ∩ t)
have rw₁ : #u = #u
Tactic: rw [← inter_union_distrib_left, inter_eq_left.2 hus]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
have obtain : ∀ (u : Finset α) (hus : u ⊆ s) (hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s) (hu : ThreeGPFree (↑u : Set α)),
  HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
Tactic: obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
have obtain : ∀ (v : Finset β) (hvt : v ⊆ t) (hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t) (hv : ThreeGPFree (↑v : Set β)),
  HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
Tactic: obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
have rw : #(u ×ˢ v) ≤ (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
Tactic: rw [← hucard, ← hvcard, ← card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
⊢ #(u ×ˢ v) ≤ (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
have refine : ThreeGPFree (↑(u ×ˢ v) : Set (α × β))
Tactic: refine ThreeGPFree.le_mulRothNumber ?_ (product_subset_product hus hvt)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
⊢ ThreeGPFree (↑(u ×ˢ v) : Set (α × β))
have rw : ThreeGPFree ((↑u : Set α) ×ˢ (↑v : Set β))
Tactic: rw [coe_product]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree (↑t : Set α)
⊢ (mulRothNumber : (a : Finset α) → ℕ) s < n
have obtain : ∀ (t : Finset α) (hts : t ⊆ s) (hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s) (ht : ThreeGPFree (↑t : Set α)),
  (mulRothNumber : (a : Finset α) → ℕ) s < n
Tactic: obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree (↑t : Set α)
t : Finset α
hts : t ⊆ s
hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s
ht : ThreeGPFree (↑t : Set α)
⊢ (mulRothNumber : (a : Finset α) → ℕ) s < n
have rw : ¬n ≤ #t
Tactic: rw [← hcard, ← not_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree (↑t : Set α)
t : Finset α
hts : t ⊆ s
hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s
ht : ThreeGPFree (↑t : Set α)
hn : n ≤ #t
⊢ False
have obtain : ∀ (u : Finset α) (hut : u ⊆ t) (h : ∀ t ∈ powersetCard (#u) s, ¬ThreeGPFree (↑t : Set α)) (hn : #u ≤ #t), False
Tactic: obtain ⟨u, hut, rfl⟩ := exists_subset_card_eq hn
Cleared hypotheses: n, h, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)
have obtain : ∀ (s : Finset β) (hsB : s ⊆ B) (hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B) (hs : ThreeGPFree (↑s : Set β)),
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)
Tactic: obtain ⟨s, hsB, hcard, hs⟩ := mulRothNumber_spec B
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)
have hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
Tactic: have hsA : invFunOn f A '' s ⊆ A :=
    (hf'.surjOn.mapsTo_invFunOn.mono (coe_subset.2 hsB) Subset.rfl).image_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)
have hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
Tactic: have hfsA : Set.SurjOn f A s := hf'.surjOn.mono Subset.rfl (coe_subset.2 hsB)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)
have rw : #(image (invFunOn f (↑A : Set α)) s) ≤ (mulRothNumber : (a : Finset α) → ℕ) A
Tactic: rw [← hcard, ← s.card_image_of_injOn ((invFunOn_injOn_image f _).mono hfsA)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
⊢ #(image (invFunOn f (↑A : Set α)) s) ≤ (mulRothNumber : (a : Finset α) → ℕ) A
have refine : ThreeGPFree (↑(image (invFunOn f (↑A : Set α)) s) : Set α)
Tactic: refine ThreeGPFree.le_mulRothNumber ?_ (mod_cast hsA)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
⊢ ThreeGPFree (↑(image (invFunOn f (↑A : Set α)) s) : Set α)
have rw : ThreeGPFree (invFunOn f (↑A : Set α) '' (↑s : Set β))
Tactic: rw [coe_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have refine : LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
Tactic: refine le_antisymm ?_ (hf.isMulFreimanHom.mulRothNumber_mono hf.bijOn)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have obtain : ∀ (s : Finset α) (hsA : s ⊆ A) (hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A) (hs : ThreeGPFree (↑s : Set α)),
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
Tactic: obtain ⟨s, hsA, hcard, hs⟩ := mulRothNumber_spec A
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : s ⊆ A
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have hsA₁ : (↑s : Set α) ⊆ (↑A : Set α)
Tactic: rw [← coe_subset] at hsA
Cleared hypotheses: hsA, hcard, hs
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have hfs : Set.InjOn f (↑s : Set α)
Tactic: have hfs : Set.InjOn f s := hf.bijOn.injOn.mono hsA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have this : ThreeGPFree (f '' (↑s : Set α))
Tactic: have := (hf.subset hsA hfs.bijOn_image).threeGPFree_congr.1 hs
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (f '' (↑s : Set α))
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have this₁ : ThreeGPFree (↑(image f s) : Set β)
Tactic: rw [← coe_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
have rw : #(image f s) ≤ (mulRothNumber : (a : Finset β) → ℕ) B
Tactic: rw [← hcard, ← Finset.card_image_of_injOn hfs]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
⊢ #(image f s) ≤ (mulRothNumber : (a : Finset β) → ℕ) B
have refine : image f s ⊆ B
Tactic: refine this.le_mulRothNumber ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
⊢ image f s ⊆ B
have rw : f '' (↑s : Set α) ⊆ (↑B : Set β)
Tactic: rw [← coe_subset, coe_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have refine_1 : LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
  ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
refine_1 :
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have refine_2 : LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
  ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have refine_1 : ∀ (u : Finset α) (hus : u ⊆ map (mulLeftEmbedding a) s)
  (hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)) (hu : ThreeGPFree (↑u : Set α)),
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
Tactic: obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s.map <| mulLeftEmbedding a)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑u : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have hus₁ : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
Tactic: rw [subset_map_iff] at hus
Cleared hypotheses: hus, hcard, hu
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑u : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have refine_1 : ∀ (u : Finset α) (hus : u ⊆ s)
  (hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s))
  (hu : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)),
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
Tactic: obtain ⟨u, hus, rfl⟩ := hus
Cleared hypotheses: u, hus, hcard, hu
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have hu₁ : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
Tactic: rw [coe_map] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have refine_1 : #u ≤ (mulRothNumber : (a : Finset α) → ℕ) s
Tactic: rw [← hcard, card_map]