awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
linarith₁ : 16 ≤ 12 * log 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
linarith₂ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 156250000 0
⊢ 12 * log 2 < 16
have linarith₃ : 16 ≤ 12 * log 2 →
  HMul.hMul (α := ℝ) 300087259 (-1) + 39062500 * (16 - 12 * log 2) +
      3 * (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247) =
    0
Tactic: linarith [log_two_lt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
linarith₁ : 16 ≤ 12 * log 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
linarith₂ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 156250000 0
linarith₃ :
  16 ≤ 12 * log 2 →
    HMul.hMul (α := ℝ) 300087259 (-1) + 39062500 * (16 - 12 * log 2) +
        3 * (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247) =
      0
⊢ 12 * log 2 < 16
have linarith₄ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 300087259 0
Tactic: linarith [log_two_lt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
linarith₁ : 16 ≤ 12 * log 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
linarith₂ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 156250000 0
linarith₃ :
  16 ≤ 12 * log 2 →
    HMul.hMul (α := ℝ) 300087259 (-1) + 39062500 * (16 - 12 * log 2) +
        3 * (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247) =
      0
linarith₄ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 300087259 0
⊢ 12 * log 2 < 16
have linarith₅ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 39062500 0
Tactic: linarith [log_two_lt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
linarith₁ : 16 ≤ 12 * log 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
linarith₂ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 156250000 0
linarith₃ :
  16 ≤ 12 * log 2 →
    HMul.hMul (α := ℝ) 300087259 (-1) + 39062500 * (16 - 12 * log 2) +
        3 * (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247) =
      0
linarith₄ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 300087259 0
linarith₅ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 39062500 0
⊢ 12 * log 2 < 16
have linarith₆ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 3 0
Tactic: linarith [log_two_lt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1
have rw : (↑N : ℝ) ≤ rexp (HPow.hPow (α := ℝ) (β := ℕ) 4 2)
Tactic: rw [← log_le_log_iff (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one,
    log_one, log_mul (cast_pos.2 (zero_lt_two.trans_le hN)).ne' (exp_pos _).ne', log_exp, neg_mul, ←
    sub_eq_add_neg, sub_nonpos, ←
    div_le_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| one_lt_two.trans_le hN), div_sqrt,
    sqrt_le_left zero_le_four, log_le_iff_le_exp (cast_pos.2 (zero_lt_two.trans_le hN))]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ (↑N : ℝ) ≤ rexp (HPow.hPow (α := ℝ) (β := ℕ) 4 2)
have norm_num1 : (↑N : ℝ) ≤ rexp 16
Tactic: norm_num1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ (↑N : ℝ) ≤ rexp 16
have apply : LE.le (α := ℝ) (↑N : ℝ) 4096
Tactic: apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 1 ≤ N
hN' : N ≤ 4096
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1
have inl : ∀ (hN : LE.le (α := ℕ) 1 1) (hN' : LE.le (α := ℕ) 1 4096), (↑1 : ℝ) * rexp (-4 * √(log (↑1 : ℝ))) ≤ 1
Tactic: obtain rfl | hN := hN.eq_or_lt
Cleared hypotheses: N, hN, hN'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 1 ≤ N
hN' : N ≤ 4096
inl : ∀ (hN : LE.le (α := ℕ) 1 1) (hN' : LE.le (α := ℕ) 1 4096), (↑1 : ℝ) * rexp (-4 * √(log (↑1 : ℝ))) ≤ 1
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1
have inr : ∀ (hN : 1 < N), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1
Tactic: obtain rfl | hN := hN.eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have inl : (↑0 : ℝ) * rexp (-4 * √(log (↑0 : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) 0) : ℝ)
Tactic: obtain rfl | hN := Nat.eq_zero_or_pos N
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
inl : (↑0 : ℝ) * rexp (-4 * √(log (↑0 : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) 0) : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have inr : ∀ (hN : N > 0), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
Tactic: obtain rfl | hN := Nat.eq_zero_or_pos N
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : N > 0
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have inr : ∀ (h₁ : 4096 ≤ N), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
Tactic: obtain h₁ | h₁ := le_or_gt 4096 N
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : N > 0
inr : ∀ (h₁ : 4096 ≤ N), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have inr₁ : ∀ (h₁ : N < 4096), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
Tactic: obtain h₁ | h₁ := le_or_gt 4096 N
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have inr : LE.le (α := ℝ) 1 (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
Tactic: apply (lower_bound_le_one hN h₁.le).trans
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b
have this : BijOn f A (f '' A)
Tactic: have := (hf.bijOn.injOn.mono hAs).bijOn_image (f := f)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree s ↔ ThreeGPFree t
have rw : ThreeGPFree (f '' s) ↔ ThreeGPFree t
Tactic: rw [← threeGPFree_image hf subset_rfl, hf.bijOn.image_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
rw : ThreeGPFree (f '' s) ↔ ThreeGPFree t
⊢ ThreeGPFree s ↔ ThreeGPFree t
have rw₁ : ThreeGPFree t ↔ ThreeGPFree t
Tactic: rw [← threeGPFree_image hf subset_rfl, hf.bijOn.image_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s : Set α
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
hf : InjOn.{u_2, u_3} (β := β) (⇑f : (a : α) → β) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a * c) : β) ((f : (a : α) → β) (b * b) : β)
have rwa : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) = (f : (a : α) → β) (b * b)
Tactic: rwa [map_mul, map_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s : Set α
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
hf : InjOn.{u_2, u_3} (β := β) (⇑f : (a : α) → β) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
Tactic: rw [h ha hb hc (hf (mul_mem_mul ha hc) (mul_mem_mul hb hb) <| by rwa [map_mul, map_mul])]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : a * c = b * b
⊢ b = c
have obtain : ∀ (hb : a ∈ s) (habc : a * c = a * a), a = c
Tactic: obtain rfl := hs ha hb hc habc
Cleared hypotheses: b, hb, habc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
⊢ ThreeGPFree (insert a s) ↔
    ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
have refine : (ThreeGPFree s ∧
    (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) →
  ThreeGPFree (insert a s)
Tactic: refine ⟨fun hs ↦ ⟨hs.mono (subset_insert _ _),
    fun b hb c hc ↦ hs (Or.inl rfl) (Or.inr hb) (Or.inr hc),
    fun b hb c hc ↦ hs (Or.inr hb) (Or.inl rfl) (Or.inr hc)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b : α
hb : b ∈ insert a s
c : α
hc : c ∈ insert a s
d : α
hd : d ∈ insert a s
h : b * d = c * c
⊢ b = c
have rw : ∀ (hb : b = a ∨ b ∈ s) ⦃c : α⦄ (hc : c = a ∨ c ∈ s) ⦃d : α⦄ (hd : d = a ∨ d ∈ s) (h : b * d = c * c), b = c
Tactic: rw [mem_insert_iff] at hb hc hd
Cleared hypotheses: hb, c, hc, d, hd, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b : α
hb : b = a ∨ b ∈ s
c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
⊢ b = c
have inl : ∀ (ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1)
  (ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b) (hc : c = b ∨ c ∈ s) (hd : d = b ∨ d ∈ s),
  b = c
Tactic: obtain rfl | hb := hb
Cleared hypotheses: a, ha, ha', hb, hc, hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b : α
hb : b = a ∨ b ∈ s
c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
inl :
  ∀ (ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1)
    (ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b) (hc : c = b ∨ c ∈ s)
    (hd : d = b ∨ d ∈ s), b = c
⊢ b = c
have inr : ∀ (hb : b ∈ s), b = c
Tactic: obtain rfl | hb := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c = b ∨ c ∈ s
hd : d = b ∨ d ∈ s
⊢ b = c
have inl : ∀ (h : c * d = c * c) (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b)
  (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c) (hd : d = c ∨ d ∈ s), c = c
Tactic: obtain rfl | hc := hc
Cleared hypotheses: b, h, ha, ha', hc, hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c = b ∨ c ∈ s
hd : d = b ∨ d ∈ s
inl :
  ∀ (h : c * d = c * c) (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b)
    (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c) (hd : d = c ∨ d ∈ s), c = c
⊢ b = c
have inl₁ : ∀ (hc : c ∈ s), b = c
Tactic: obtain rfl | hc := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
⊢ b = c
have inr : ∀ (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b)
  (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c) (hd : d = c ∨ d ∈ s), b = c
Tactic: obtain rfl | hc := hc
Cleared hypotheses: a, ha, ha', hc, hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
inr :
  ∀ (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b)
    (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c) (hd : d = c ∨ d ∈ s), b = c
⊢ b = c
have inr₁ : ∀ (hc : c ∈ s), b = c
Tactic: obtain rfl | hc := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hd : d = b ∨ d ∈ s
hc : c ∈ s
⊢ b = c
have inl : ∀ (h : d * d = c * c) (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b)
  (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d), d = c
Tactic: obtain rfl | hd := hd
Cleared hypotheses: b, h, ha, ha', hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hd : d = b ∨ d ∈ s
hc : c ∈ s
inl :
  ∀ (h : d * d = c * c) (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b)
    (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d), d = c
⊢ b = c
have inl₁ : ∀ (hd : d ∈ s), b = c
Tactic: obtain rfl | hd := hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
⊢ b = c
have inr : ∀ (h : b * d = d * d) (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b)
  (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d), b = d
Tactic: obtain rfl | hd := hd
Cleared hypotheses: c, h, ha, ha', hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
inr :
  ∀ (h : b * d = d * d) (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b)
    (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d), b = d
⊢ b = c
have inr₁ : ∀ (hd : d ∈ s), b = c
Tactic: obtain rfl | hd := hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
⊢ b = c
have inr : ∀ (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b)
  (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d), b = c
Tactic: obtain rfl | hd := hd
Cleared hypotheses: a, ha, ha', hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
inr :
  ∀ (ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b)
    (ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d), b = c
⊢ b = c
have inr₁ : ∀ (hd : d ∈ s), b = c
Tactic: obtain rfl | hd := hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c
have inr : ∀ (h : b * d = d * d) (hc : d ∈ s), b = d
Tactic: obtain rfl := ha hc hb ((mul_comm _ _).trans h)
Cleared hypotheses: c, h, hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a • b * a • d = a * c * (a * c)
have rw : a • b * a • d = a * a * (c * c)
Tactic: rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
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 * a * (c * c)
⊢ a • b * a • d = a * c * (a * c)
have rw₁ : a * b * a • d = a * a * (c * c)
Tactic: rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
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 * a * (c * c)
rw₁ : a * b * a • d = a * a * (c * c)
⊢ a • b * a • d = a * c * (a * c)
have rw₂ : a * b * (a * d) = a * a * (c * c)
Tactic: rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
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 * a * (c * c)
rw₁ : a * b * a • d = a * a * (c * c)
rw₂ : a * b * (a * d) = a * a * (c * c)
⊢ a • b * a • d = a * c * (a * c)
have rw₃ : a * a * (b * d) = a * a * (c * c)
Tactic: rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
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 * a * (c * c)
rw₁ : a * b * a • d = a * a * (c * c)
rw₂ : a * b * (a * d) = a * a * (c * c)
rw₃ : a * a * (b * d) = a * a * (c * c)
⊢ a • b * a • d = a * c * (a * c)
have rw₄ : a * a * (c * c) = a * a * (c * c)
Tactic: rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
have refine : (ThreeGPFree s ∧
    (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
  ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
Tactic: refine threeGPFree_insert.trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ (ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
have rw : ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
    ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
  ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
Tactic: rw [← and_assoc]
-- 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
⊢ a • b * a • d = a * c * (a * c)
have rw : a * b * a • d = 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)
⊢ a • b * a • d = a * c * (a * c)
have rw₁ : a * b * (a * d) = 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)
⊢ a • b * a • d = a * c * (a * c)
have rw₂ : a * a * (b * d) = a * c * (a * c)
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]