awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
⊢ 0 < √(log (↑N : ℝ))

Tactic:
Real.sqrt_pos.2 (log_pos ?_)

Premises used: Iff.mpr, Real.log_pos, Real.sqrt_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc : LT.lt (α := ℝ) 1 (↑N : ℝ)
⊢ 0 < √(log (↑N : ℝ))

Tactic:
refine Real.sqrt_pos.2 (log_pos ?_)

Premises used: Iff.mpr, Real.log_pos, Real.sqrt_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc : 1 < N
⊢ LT.lt (α := ℝ) 1 (↑N : ℝ)

Tactic:
rw [one_lt_cast]

Premises used: Nat.one_lt_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
⊢ LT.lt (α := ℕ) 1 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
⊢ 1 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

Premises used: LE.le.trans_lt'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
⊢ rexp (-2 * √(log (↑N : ℝ))) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ)

Tactic:
(exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos ?_).le

Premises used: Iff.mpr, Real.log_pos, LT.lt.le, Behrend.exp_neg_two_mul_le, Real.sqrt_pos, Behrend.nValue
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc : LT.lt (α := ℝ) 1 (↑N : ℝ)
⊢ rexp (-2 * √(log (↑N : ℝ))) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ)

Tactic:
refine (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos ?_).le

Premises used: Iff.mpr, Real.log_pos, LT.lt.le, Behrend.exp_neg_two_mul_le, Real.sqrt_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
rw : 64 = HPow.hPow (α := ℝ) (β := ℕ) 2 6
⊢ 64 = HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ)

Tactic:
rw [rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ 64 = HPow.hPow (α := ℝ) (β := ℕ) 2 6

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
rw : HDiv.hDiv (α := ℝ) 4 (↑6 : ℝ) < log 2
rw₁ : LT.lt (α := ℝ) 0 (↑6 : ℝ)
⊢ rexp 4 < 64

Tactic:
rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1,
    ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀']

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, Real.lt_log_iff_exp_lt, div_lt_iff₀', zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ HDiv.hDiv (α := ℝ) 4 (↑6 : ℝ) ≤ 0.6931471803

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ HDiv.hDiv (α := ℝ) 4 (↑6 : ℝ) < log 2

Tactic:
exact log_two_gt_d9.trans_le' (by norm_num1)

Premises used: Real.log_two_gt_d9, LT.lt.trans_le'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ LT.lt (α := ℝ) 0 (↑6 : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ LT.lt (α := ℝ) 0 4096

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 4096 = HPow.hPow (α := ℕ) (β := ℕ) 2 12
⊢ 4096 = HPow.hPow (α := ℝ) (β := ℕ) 2 12

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
rw : 12 * log 2 < 16
⊢ 4096 < rexp 16

Tactic:
rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by simp), show (4096 : ℝ) = 2 ^ 12 by norm_cast,
    ← rpow_natCast, log_rpow zero_lt_two, cast_ofNat]

Premises used: Nat.cast_ofNat, Real.log_rpow, Real.log_lt_iff_lt_exp, zero_lt_two, Real.rpow_natCast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
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
linarith₆ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 3 0
⊢ 12 * log 2 < 16

Tactic:
linarith [log_two_lt_d9]

Premises used: Real.log_two_lt_d9
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
rw : (↑N : ℝ) ≤ rexp (HPow.hPow (α := ℝ) (β := ℕ) 4 2)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1

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))]

Premises used: Iff.mpr, div_le_iff₀, Nat.cast_pos, Real.log_exp, sub_eq_add_neg, Real.log_one, Real.log_pos, zero_le_four, Real.log_le_iff_le_exp, LT.lt.ne', Real.div_sqrt, zero_lt_one, mul_pos, Real.sqrt_pos, Real.log_le_log_iff, LT.lt.trans_le, Real.sqrt_le_left, Nat.one_lt_cast, one_lt_two, neg_mul, sub_nonpos, zero_lt_two, Real.log_mul, Real.exp_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
norm_num1 : (↑N : ℝ) ≤ rexp 16
⊢ (↑N : ℝ) ≤ rexp (HPow.hPow (α := ℝ) (β := ℕ) 4 2)

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
apply : LE.le (α := ℝ) (↑N : ℝ) 4096
⊢ (↑N : ℝ) ≤ rexp 16

Tactic:
apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le

Premises used: Behrend.four_zero_nine_six_lt_exp_sixteen, LT.lt.le, le_trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ LE.le (α := ℝ) (↑N : ℝ) 4096

Tactic:
mod_cast hN'

Premises used: cast, Nat.cast_le._simp_1, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ LE.le (α := ℝ) (↑N : ℝ) 4096

Tactic:
exact mod_cast hN'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
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
inr : ∀ (hN : 1 < N), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1

Tactic:
obtain rfl | hN := hN.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
hN : LE.le (α := ℕ) 1 1
hN' : LE.le (α := ℕ) 1 4096
⊢ (↑1 : ℝ) * rexp (-4 * √(log (↑1 : ℝ))) ≤ 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN_1 : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1

Tactic:
lower_bound_le_one' hN hN'

Premises used: Behrend.lower_bound_le_one'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN_1 : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ 1

Tactic:
exact lower_bound_le_one' hN hN'

Premises used: Behrend.lower_bound_le_one'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
inl : (↑0 : ℝ) * rexp (-4 * √(log (↑0 : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) 0) : ℝ)
inr : ∀ (hN : N > 0), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
obtain rfl | hN := Nat.eq_zero_or_pos N

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ (↑0 : ℝ) * rexp (-4 * √(log (↑0 : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) 0) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : N > 0
inr : ∀ (h₁ : 4096 ≤ N), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
inr₁ : ∀ (h₁ : N < 4096), (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
obtain h₁ | h₁ := le_or_gt 4096 N

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
(roth_lower_bound_explicit h₁).le

Premises used: Behrend.roth_lower_bound_explicit, LT.lt.le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
exact (roth_lower_bound_explicit h₁).le

Premises used: Behrend.roth_lower_bound_explicit, LT.lt.le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : N > 0
h₁ : N < 4096
inr : LE.le (α := ℝ) 1 (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
apply (lower_bound_le_one hN h₁.le).trans

Premises used: Behrend.lower_bound_le_one, LT.lt.le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ LE.le (α := ℝ) 1 (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
simpa using rothNumberNat.monotone hN

Premises used: OrderHom.monotone, rothNumberNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
h : t ⊆ s
hs : ThreeGPFree s
⊢ ThreeGPFree t

Tactic:
fun _ ha _ hb _ hc ↦ hs (h ha) (h hb) (h hc)

Premises used: ThreeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : Monoid α
⊢ ThreeGPFree.{u_2} (α := α) ∅

Tactic:
fun _ _ _ ha => ha.elim

Premises used: False.elim, ThreeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : s.Subsingleton
⊢ ThreeGPFree s

Tactic:
fun _ ha _ hb _ _ _ ↦ hs ha hb

Premises used: ThreeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : Monoid α
a : α
⊢ ThreeGPFree (α := α) {a}

Tactic:
subsingleton_singleton.threeGPFree

Premises used: Set.subsingleton_singleton, Set.Subsingleton.threeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
s : Set α
t : Set β
hs : ThreeGPFree s
ht : ThreeGPFree t
⊢ ThreeGPFree (s ×ˢ t)

Tactic:
fun _ ha _ hb _ hc h ↦
  Prod.ext (hs ha.1 hb.1 hc.1 (Prod.ext_iff.1 h).1) (ht ha.2 hb.2 hc.2 (Prod.ext_iff.1 h).2)

Premises used: Prod.ext_iff, And.right, And.left, Prod.ext, Iff.mp, ThreeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → Monoid (α i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), ThreeGPFree (s i)
⊢ ThreeGPFree (Set.pi (α := α) Set.univ s)

Tactic:
fun _ ha _ hb _ hc h ↦
  funext fun i => hs i (ha i trivial) (hb i trivial) (hc i trivial) <| congr_fun h i

Premises used: trivial, funext, congr_fun, ThreeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanHom 2 s t f
hf' : InjOn f s
hAs : A ⊆ s
hA : ThreeGPFree (f '' A)
⊢ ThreeGPFree A

Tactic:
fun _ ha _ hb _ hc habc ↦ hf' (hAs ha) (hAs hb) <| hA (mem_image_of_mem _ ha)
    (mem_image_of_mem _ hb) (mem_image_of_mem _ hc) <|
    hf.mul_eq_mul (hAs ha) (hAs hc) (hAs hb) (hAs hb) habc

Premises used: IsMulFreimanHom.mul_eq_mul, Set.mem_image_of_mem, ThreeGPFree
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
⊢ BijOn f A (f '' A)

Tactic:
have := (hf.bijOn.injOn.mono hAs).bijOn_image (f := f)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
this : BijOn f A (f '' A)
⊢ (∀ ⦃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

Tactic:
simp +contextual only
    [((hf.bijOn.injOn.mono hAs).bijOn_image (f := f)).forall,
    hf.mul_eq_mul (hAs _) (hAs _) (hAs _) (hAs _), this.injOn.eq_iff]

Premises used: Set.InjOn.eq_iff, IsMulFreimanIso.bijOn, IsMulFreimanIso.mul_eq_mul, Set.InjOn.bijOn_image, Set.BijOn.injOn, Set.BijOn.forall, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanHom 2 s t f
hf' : InjOn f s
ht : ThreeGPFree t
⊢ ThreeGPFree s

Tactic:
(ht.mono hf.mapsTo.image_subset).of_image hf hf' subset_rfl

Premises used: IsMulFreimanHom.mapsTo, ThreeGPFree.mono, ThreeGPFree.of_image, Set.MapsTo.image_subset, subset_rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
rw₁ rw₂ : ThreeGPFree t ↔ ThreeGPFree t
⊢ ThreeGPFree s ↔ ThreeGPFree t

Tactic:
rw [← threeGPFree_image hf subset_rfl, hf.bijOn.image_eq]

Premises used: IsMulFreimanIso.bijOn, Set.BijOn.image_eq, subset_rfl, threeGPFree_image
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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 : β)
rwa : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) = (f : (a : α) → β) (b * b)
rwa₁ rwa₂ rwa₃ rwa₄ :
  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) : β)

Tactic:
rwa [map_mul, map_mul]

Premises used: map_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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 : β)
rw rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((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])]

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
obtain : ∀ (hb : a ∈ s) (habc : a * c = a * a), a = c
⊢ b = c

Tactic:
obtain rfl := hs ha hb hc habc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
c : α
hc : c ∈ s
hb : a ∈ s
habc : a * c = a * a
⊢ a = c

Tactic:
simpa using habc.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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

Tactic:
⟨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)⟩, ?_⟩

Premises used: ThreeGPFree.mono, And.intro, Iff.intro, Or.inl, Set.subset_insert, Or.inr, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
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)
⊢ 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

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)⟩, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
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
⊢ b = c

Tactic:
rw [mem_insert_iff] at hb hc hd

Premises used: Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
inr : ∀ (hb : b ∈ s), b = c
⊢ b = c

Tactic:
obtain rfl | hb := hb

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
inl₁ : ∀ (hc : c ∈ s), b = c
⊢ b = c

Tactic:
obtain rfl | hc := hc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
inr₁ : ∀ (hc : c ∈ s), b = c
⊢ b = c

Tactic:
obtain rfl | hc := hc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
c d : α
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:
rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
inl₁ : ∀ (hd : d ∈ s), b = c
⊢ b = c

Tactic:
obtain rfl | hd := hd

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
inr₁ : ∀ (hd : d ∈ s), b = c
⊢ b = c

Tactic:
obtain rfl | hd := hd

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
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
inr₁ : ∀ (hd : d ∈ s), b = c
⊢ b = c

Tactic:
obtain rfl | hd := hd

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
c d : α
hc : c ∈ s
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:
(ha' hc hc h.symm).symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
c d : α
hc : c ∈ s
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:
exact (ha' hc hc h.symm).symm

Premises used: Eq.symm