awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) = ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
hbc : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) ≤ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
hbc : 1 ≤ n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 3 / 9) * 27)⁻¹⌋₊ + 1 ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) = ε * (↑n : ℝ)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)

Tactic:
hAε
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
rw : Set.InjOn (β := Fin (2 * n + 1)) (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) (↑A : Set ℕ)
⊢ Eq (α := ℝ) (↑(#A) : ℝ) (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)

Tactic:
rw [card_image_of_injOn]

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
simp : n ≤ 2 * n + 1
⊢ Set.Iio n ⊆ Set.Iio (2 * n).succ

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ n ≤ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
⊢ Set.InjOn (β := Fin (2 * n + 1)) (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) (↑A : Set ℕ)

Tactic:
exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia

Premises used: HMul.hMul, CharP.natCast_injOn_Iio, HasSubset.Subset.trans, Set.InjOn.mono, OfNat.ofNat, Fin, Nat.succ
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
_ : ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) = ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
_₁ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) ≤ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ))
_₂ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) = ε * (↑n : ℝ)
_₃ :
  Eq (α := ℝ) (↑(#A) : ℝ) (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
⊢ ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
    (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)

Tactic:
calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
simp : ∀ ⦃c : ℝ⦄, 0 < c → ∃ (a : ℕ), ∀ b ≥ a, (↑((rothNumberNat : (a : ℕ) → ℕ) b) : ℝ) ≤ c * (↑b : ℝ)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (N : ℕ) ↦ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)) fun (N : ℕ) ↦ (↑N : ℝ)

Tactic:
simp only [isLittleO_iff, eventually_atTop, RCLike.norm_natCast]

Premises used: RCLike.norm_natCast, Asymptotics.isLittleO_iff, Filter.eventually_atTop
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∃ (a : ℕ), ∀ b ≥ a, (↑((rothNumberNat : (a : ℕ) → ℕ) b) : ℝ) ≤ c * (↑b : ℝ)

Tactic:
fun ε hε ↦ ⟨cornersTheoremBound (ε / 3), fun n hn ↦ ?_⟩

Premises used: HDiv.hDiv, cornersTheoremBound, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
refine :
  ∀ (ε : ℝ) (hε : 0 < ε) (n : ℕ) (hn : n ≥ cornersTheoremBound (ε / 3)),
    (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∃ (a : ℕ), ∀ b ≥ a, (↑((rothNumberNat : (a : ℕ) → ℕ) b) : ℝ) ≤ c * (↑b : ℝ)

Tactic:
refine fun ε hε ↦ ⟨cornersTheoremBound (ε / 3), fun n hn ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
obtain :
  ∀ (A : Finset ℕ) (hs₁ : A ⊆ range n) (hs₂ : #A = (rothNumberNat : (a : ℕ) → ℕ) n) (hs₃ : ThreeAPFree (↑A : Set ℕ)),
    (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)
⊢ (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)

Tactic:
obtain ⟨A, hs₁, hs₂, hs₃⟩ := rothNumberNat_spec n

Premises used: rothNumberNat_spec
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = (rothNumberNat : (a : ℕ) → ℕ) n
hs₃ : ThreeAPFree (↑A : Set ℕ)
rw : ¬ε * (↑n : ℝ) < (↑(#A) : ℝ)
⊢ (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)

Tactic:
rw [← hs₂, ← not_lt]

Premises used: not_lt
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = (rothNumberNat : (a : ℕ) → ℕ) n
hs₃ : ThreeAPFree (↑A : Set ℕ)
⊢ ¬ε * (↑n : ℝ) < (↑(#A) : ℝ)

Tactic:
fun hδn ↦ roth_3ap_theorem_nat ε hε hn _ hs₁ hδn.le hs₃

Premises used: LT.lt.le, roth_3ap_theorem_nat, Not
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = (rothNumberNat : (a : ℕ) → ℕ) n
hs₃ : ThreeAPFree (↑A : Set ℕ)
⊢ ¬ε * (↑n : ℝ) < (↑(#A) : ℝ)

Tactic:
exact fun hδn ↦ roth_3ap_theorem_nat ε hε hn _ hs₁ hδn.le hs₃

Premises used: roth_3ap_theorem_nat
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
A : Set X
⊢ LE.le (α := ℝ) (↑(Finset.card.{u_1} (α := M) 1) : ℝ) 1 ∧ A ⊆ (↑1 : Set M) • A

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
A B : Set X
hAB : A ⊆ B
⊢ LE.le (α := ℝ) (↑(Finset.card.{u_1} (α := M) 1) : ℝ) 1 ∧ A ⊆ (↑1 : Set M) • B

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K : ℝ
A B : Set X
F : Finset M
hF : (↑(#F) : ℝ) ≤ K
⊢ 0 ≤ K

Tactic:
(#F).cast_nonneg.trans hF

Premises used: Nat.cast_nonneg, Finset.card, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K : ℝ
A B : Set X
F : Finset M
hF : (↑(#F) : ℝ) ≤ K
⊢ 0 ≤ K

Tactic:
exact (#F).cast_nonneg.trans hF

Premises used: Nat.cast_nonneg, Finset.card, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
A B : Set X
⊢ CovBySMul M 0 A B ↔ A = ∅

Tactic:
simp [CovBySMul]

Premises used: CovBySMul
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K L : ℝ
A B : Set X
hKL : K ≤ L
F : Finset M
hF : (↑(#F) : ℝ) ≤ K
hFAB : A ⊆ (↑F : Set M) • B
⊢ CovBySMul M L A B

Tactic:
⟨F, hF.trans hKL, hFAB⟩

Premises used: CovBySMul, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K L : ℝ
A B : Set X
hKL : K ≤ L
F : Finset M
hF : (↑(#F) : ℝ) ≤ K
hFAB : A ⊆ (↑F : Set M) • B
⊢ CovBySMul M L A B

Tactic:
exact ⟨F, hF.trans hKL, hFAB⟩
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
⊢ 0 ≤ K

Tactic:
have := hAB.nonneg
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
this : 0 ≤ K
obtain : ∀ (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
⊢ CovBySMul N (K * L) A C

Tactic:
obtain ⟨F₁, hF₁, hFAB⟩ := hAB
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hBC : CovBySMul N L B C
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
obtain : ∀ (F₂ : Finset N) (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), CovBySMul N (K * L) A C
⊢ CovBySMul N (K * L) A C

Tactic:
obtain ⟨F₂, hF₂, hFBC⟩ := hBC
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ CovBySMul N (K * L) A C

Tactic:
⟨F₁ • F₂, ?_, ?_⟩

Premises used: CovBySMul, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
refine_1 : (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
refine_2 : A ⊆ (↑(F₁ • F₂) : Set N) • C
⊢ CovBySMul N (K * L) A C

Tactic:
refine ⟨F₁ • F₂, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ (↑(#(F₁ • F₂)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#F₁) : ℝ) (↑(#F₂) : ℝ)

Tactic:
mod_cast Finset.card_smul_le

Premises used: Nat.cast_mul._simp_1, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card, HSMul.hSMul, Finset.card_smul_le, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
c0 : LE.le (α := ℝ) 0 (↑(#F₂) : ℝ)
b0 : 0 ≤ K
⊢ HMul.hMul (α := ℝ) (↑(#F₁) : ℝ) (↑(#F₂) : ℝ) ≤ K * L

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
mod_cast : HMul.hMul (α := ℝ) (↑(#F₁) : ℝ) (↑(#F₂) : ℝ) ≤ K * L
⊢ (↑(#(F₁ • F₂)) : ℝ) ≤ K * L

Tactic:
calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr

Premises used: Nat.cast, Finset.card, HSMul.hSMul, Finset.card_smul_le
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ A ⊆ (↑F₁ : Set M) • B

Tactic:
hFAB
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ (↑F₁ : Set M) • B ⊆ (↑F₁ : Set M) • (↑F₂ : Set N) • C

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ (↑F₁ : Set M) • (↑F₂ : Set N) • C = (↑(F₁ • F₂) : Set N) • C

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
A₁ : (↑F₁ : Set M) • B ⊆ (↑F₁ : Set M) • (↑F₂ : Set N) • C
A₂ : (↑F₁ : Set M) • (↑F₂ : Set N) • C = (↑(F₁ • F₂) : Set N) • C
⊢ A ⊆ (↑(F₁ • F₂) : Set N) • C

Tactic:
calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp

Premises used: SetLike.coe, HSMul.hSMul
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
have have₁ have₂ : ∀ (this : 0 ≤ K), CovBySMul N (K * L) A C
have₃ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
have₄ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
    (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), CovBySMul N (K * L) A C
refine_1 :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
    (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
refine_2 refine_2₁ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
    (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), A ⊆ (↑(F₁ • F₂) : Set N) • C
⊢ CovBySMul N (K * L) A C

Tactic:
classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp

Premises used: Finset.card_smul_le
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K : ℝ
A₁ A₂ B : Set X
hA : A₁ ⊆ A₂
hAB : CovBySMul M K A₂ B
⊢ CovBySMul M K A₁ B

Tactic:
simpa using (CovBySMul.of_subset (M := M) hA).trans hAB

Premises used: CovBySMul.trans, CovBySMul.of_subset
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K : ℝ
A B₁ B₂ : Set X
hB : B₁ ⊆ B₂
hAB : CovBySMul M K A B₁
⊢ CovBySMul M K A B₂

Tactic:
simpa using hAB.trans (.of_subset (M := M) hB)

Premises used: CovBySMul.trans, CovBySMul.of_subset
-- Module: Mathlib.Combinatorics.Additive.CovBySMul
Goal:
M : Type u_1
X : Type u_3
inst : Monoid M
inst_1 : MulAction M X
K : ℝ
A₁ A₂ B₁ B₂ : Set X
hA : A₁ ⊆ A₂
hB : B₁ ⊆ B₂
hAB : CovBySMul M K A₂ B₁
⊢ CovBySMul M K A₁ B₂

Tactic:
(hAB.subset_left hA).subset_right hB

Premises used: CovBySMul.subset_right, CovBySMul.subset_left
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
⊢ MulDissociated s ↔
    ∀ (a : α), Set.Subsingleton.{u_1} (α := Finset α) {t : Finset α | (↑t : Set α) ⊆ s ∧ ∏ x ∈ t, x = a}

Tactic:
⟨fun hs _ _t ht _u hu ↦ hs ht.1 hu.1 <| ht.2.trans hu.2.symm,
    fun hs _t ht _u hu htu ↦ hs _ ⟨ht, htu⟩ ⟨hu, rfl⟩⟩

Premises used: Finset.prod, And.right, And.left, And.intro, Iff.intro, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s t : Set α
hst : s ⊆ t
ht : MulDissociated t
⊢ MulDissociated s

Tactic:
ht.mono fun _ ↦ hst.trans'

Premises used: MulDissociated, Set.InjOn.mono, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
⊢ MulDissociated.{u_1} (α := α) ∅

Tactic:
simp [MulDissociated, subset_empty_iff]

Premises used: MulDissociated, Set.subset_empty_iff
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
a : α
⊢ MulDissociated (α := α) {a} ↔ a ≠ 1

Tactic:
simp [MulDissociated, setOf_or, -subset_singleton_iff,
    Finset.coe_subset_singleton]

Premises used: Set.subset_singleton_iff, MulDissociated, Set.setOf_or, Finset.coe_subset_singleton
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α),
      (↑t : Set α) ⊆ s ∧ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ t ≠ u ∧ Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)

Tactic:
grind [MulDissociated, InjOn]

Premises used: MulDissociated, Set.InjOn
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
not_mulDissociated.trans
    ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩

Premises used: not_mulDissociated, _private.0.not_mulDissociated_iff_exists_disjoint.match_1, Exists, HasSubset.Subset, Ne, Finset.prod, And, SetLike.coe, And.intro, Iff.intro, Exists.intro, Iff.trans, Eq