awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : ∀ (hstg : #(s, t).1 + #(s, t).2 ≤ #(mulETransformLeft g (s, t)).1 + #(mulETransformLeft g (s, t)).2),
  minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
inr :
  ∀ (hstg : #(s, t).1 + #(s, t).2 ≤ #(mulETransformLeft g (s, t)).1 + #(mulETransformLeft g (s, t)).2),
    minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr₁ : ∀ (hstg : #(s, t).1 + #(s, t).2 < #(mulETransformRight g (s, t)).1 + #(mulETransformRight g (s, t)).2),
  minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #s + #t - 1 ≤ #(s * t)
have rw : #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)
Tactic: rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht),
      ← card_union_add_card_inter, ← card_singleton _, ← this, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ #s + #t - 1 ≤ #(s * t)
have suffices : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
Tactic: suffices s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht} by
    rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht),
      ← card_union_add_card_inter, ← card_singleton _, ← this, Nat.add_sub_cancel]
    exact card_mono (union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
      mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
have refine : ∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht
Tactic: refine eq_singleton_iff_unique_mem.2 ⟨mem_inter.2 ⟨mul_mem_mul (max'_mem _ _) <|
    mem_singleton_self _, mul_mem_mul (mem_singleton_self _) <| min'_mem _ _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht
have simp : ∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs
Tactic: simp only [mem_inter, and_imp, mem_mul, mem_singleton, exists_eq_left,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mul_left_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x y : G
⊢ Set.MapsTo (fun (ab' : G × G) ↦ x •> ab'.1) (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x⁻¹ * y}) : Set (G × G))
    (↑(x •> A ∩ y •> B) : Set G)
have simp : ∀ (a b : G), a ∈ A → b⁻¹ ∈ B → a * b = x⁻¹ * y → y⁻¹ * (x * a) ∈ B
Tactic: simp +contextual [Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≠ 0 ↔ x ∈ A * B
have suffices : A.convolution B x ≠ 0 ↔ 0 < A.convolution B x
Tactic: suffices A.convolution B x ≠ 0 ↔ 0 < A.convolution B x by simp [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≤ #A
have rw : #(A ∩ x •> B⁻¹) ≤ #A
Tactic: rw [← inv_inv B, ← card_inter_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≤ #B
have rw : #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹
Tactic: rw [← inv_inv B, ← inv_inv x, ← card_smul_inter, card_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x⁻¹ = B⁻¹.convolution A⁻¹ x
have nth_rw : A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
Tactic: nth_rw 1 [← inv_inv B]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
have rw : #(x •> A ∩ B⁻¹) = B⁻¹.convolution A⁻¹ x
Tactic: rw [← card_smul_inter, ← card_inter_smul, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
rw : #(x •> A ∩ B⁻¹) = B⁻¹.convolution A⁻¹ x
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
have rw₁ : #(x •> A ∩ B⁻¹) = #(B⁻¹ ∩ x •> A)
Tactic: rw [← card_smul_inter, ← card_inter_smul, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
rw : #(x •> A ∩ B⁻¹) = B⁻¹.convolution A⁻¹ x
rw₁ : #(x •> A ∩ B⁻¹) = #(B⁻¹ ∩ x •> A)
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
have rw₂ : #(B⁻¹ ∩ x •> A) = #(B⁻¹ ∩ x •> A)
Tactic: rw [← card_smul_inter, ← card_inter_smul, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
⊢ (A <• s).convolution B x = A.convolution (s •> B) x
have nth_rw : #(A <• s ∩ x •> B⁻¹) = #(A ∩ x •> B⁻¹ <• s⁻¹)
Tactic: nth_rw 1 [← inv_inv B, ← inv_inv (s • B), inv_smul_finset_distrib s B, ← card_inter_smul,
    ← card_inter_smul, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x = A.convolution B (s⁻¹ * x)
have nth_rw : (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
Tactic: nth_rw 1 [← inv_inv x, ← inv_inv (s⁻¹ * x)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
have rw : (s •> A).convolution B⁻¹⁻¹ x⁻¹⁻¹ = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
Tactic: rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : (s •> A).convolution B⁻¹⁻¹ x⁻¹⁻¹ = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
have rw₁ : #(x⁻¹ •> s •> A ∩ B⁻¹) = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
Tactic: rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : (s •> A).convolution B⁻¹⁻¹ x⁻¹⁻¹ = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₁ : #(x⁻¹ •> s •> A ∩ B⁻¹) = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
have rw₂ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((s⁻¹ * x)⁻¹ •> A ∩ B⁻¹)
Tactic: rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : (s •> A).convolution B⁻¹⁻¹ x⁻¹⁻¹ = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₁ : #(x⁻¹ •> s •> A ∩ B⁻¹) = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₂ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((s⁻¹ * x)⁻¹ •> A ∩ B⁻¹)
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
have rw₃ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s⁻¹⁻¹) •> A ∩ B⁻¹)
Tactic: rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : (s •> A).convolution B⁻¹⁻¹ x⁻¹⁻¹ = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₁ : #(x⁻¹ •> s •> A ∩ B⁻¹) = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₂ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((s⁻¹ * x)⁻¹ •> A ∩ B⁻¹)
rw₃ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s⁻¹⁻¹) •> A ∩ B⁻¹)
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
have rw₄ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s) •> A ∩ B⁻¹)
Tactic: rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : (s •> A).convolution B⁻¹⁻¹ x⁻¹⁻¹ = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₁ : #(x⁻¹ •> s •> A ∩ B⁻¹) = A.convolution B⁻¹⁻¹ (s⁻¹ * x)⁻¹⁻¹
rw₂ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((s⁻¹ * x)⁻¹ •> A ∩ B⁻¹)
rw₃ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s⁻¹⁻¹) •> A ∩ B⁻¹)
rw₄ : #(x⁻¹ •> s •> A ∩ B⁻¹) = #((x⁻¹ * s) •> A ∩ B⁻¹)
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
have rw₅ : #((x⁻¹ * s) •> A ∩ B⁻¹) = #((x⁻¹ * s) •> A ∩ B⁻¹)
Tactic: rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B (x * s⁻¹)
have nth_rw : A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Tactic: nth_rw 2 [← inv_inv B]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
have rw : A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Tactic: rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
    smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
have rw₁ : A.convolution (s⁻¹ •> B⁻¹)⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Tactic: rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
    smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
rw₁ : A.convolution (s⁻¹ •> B⁻¹)⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
have rw₂ : #(A ∩ x •> s⁻¹ •> B⁻¹) = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Tactic: rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
    smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
rw₁ : A.convolution (s⁻¹ •> B⁻¹)⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
rw₂ : #(A ∩ x •> s⁻¹ •> B⁻¹) = A.convolution B⁻¹⁻¹ (x * s⁻¹)
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
have rw₃ : #(A ∩ x •> s⁻¹ •> B⁻¹) = #(A ∩ (x * s⁻¹) •> B⁻¹)
Tactic: rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
    smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Convolution (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
rw : A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
rw₁ : A.convolution (s⁻¹ •> B⁻¹)⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
rw₂ : #(A ∩ x •> s⁻¹ •> B⁻¹) = A.convolution B⁻¹⁻¹ (x * s⁻¹)
rw₃ : #(A ∩ x •> s⁻¹ •> B⁻¹) = #(A ∩ (x * s⁻¹) •> B⁻¹)
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
have rw₄ : #(A ∩ (x * s⁻¹) •> B⁻¹) = #(A ∩ (x * s⁻¹) •> B⁻¹)
Tactic: rw [← inv_inv (B <• s), inv_op_smul_finset_distrib, ← card_inter_smul, ← card_inter_smul,
    smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hA : IsCorner A x₁ y₁ x₂ y₂
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)
have hx₁y₁ : (x₁, y₁) ∈ A
Tactic: obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hA : IsCorner A x₁ y₁ x₂ y₂
hx₁y₁ : (x₁, y₁) ∈ A
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)
have hx₁y₂ : (x₁, y₂) ∈ A
Tactic: obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hA : IsCorner A x₁ y₁ x₂ y₂
hx₁y₁ : (x₁, y₁) ∈ A
hx₁y₂ : (x₁, y₂) ∈ A
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)
have hx₂y₁ : (x₂, y₁) ∈ A
Tactic: obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hA : IsCorner A x₁ y₁ x₂ y₂
hx₁y₁ : (x₁, y₁) ∈ A
hx₁y₂ : (x₁, y₂) ∈ A
hx₂y₁ : (x₂, y₁) ∈ A
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)
have hxy : x₁ + y₂ = x₂ + y₁
Tactic: obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂
have hf' : InjOn.{u_1, u_2} (β := H × H) (fun (x : G × G) ↦ (f x.1, f x.2)) (s ×ˢ s)
Tactic: have hf' := hf.bijOn.injOn.prodMap hf.bijOn.injOn
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn.{u_1, u_2} (β := H × H) (fun (x : G × G) ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂
have rw : (f x₁, f y₁) ∈ Prod.map f f '' A ∧
    (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
  (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
Tactic: rw [isCorner_iff, isCorner_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn.{u_1, u_2} (β := H × H) (fun (x : G × G) ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
have a : (f x₁, f y₁) ∈ Prod.map f f '' A ↔ (x₁, y₁) ∈ A
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn.{u_1, u_2} (β := H × H) (fun (x : G × G) ↦ (f x.1, f x.2)) (s ×ˢ s)
a : (f x₁, f y₁) ∈ Prod.map f f '' A ↔ (x₁, y₁) ∈ A
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
have a₁ : (f x₁, f y₂) ∈ Prod.map f f '' A ↔ (x₁, y₂) ∈ A
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn.{u_1, u_2} (β := H × H) (fun (x : G × G) ↦ (f x.1, f x.2)) (s ×ˢ s)
a : (f x₁, f y₁) ∈ Prod.map f f '' A ↔ (x₁, y₁) ∈ A
a₁ : (f x₁, f y₂) ∈ Prod.map f f '' A ↔ (x₁, y₂) ∈ A
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
have a₂ : (f x₂, f y₁) ∈ Prod.map f f '' A ↔ (x₂, y₁) ∈ A
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn.{u_1, u_2} (β := H × H) (fun (x : G × G) ↦ (f x.1, f x.2)) (s ×ˢ s)
a : (f x₁, f y₁) ∈ Prod.map f f '' A ↔ (x₁, y₁) ∈ A
a₁ : (f x₁, f y₂) ∈ Prod.map f f '' A ↔ (x₁, y₂) ∈ A
a₂ : (f x₂, f y₁) ∈ Prod.map f f '' A ↔ (x₂, y₁) ∈ A
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
have a₃ : f x₁ + f y₂ = f x₂ + f y₁ ↔ x₁ + y₂ = x₂ + y₁
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
⊢ IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A
have this : Prod.map f f '' A ⊆ t ×ˢ t
Tactic: have : Prod.map f f '' A ⊆ t ×ˢ t :=
    ((hf.bijOn.mapsTo.prodMap hf.bijOn.mapsTo).mono hAs Subset.rfl).image_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A
have rw : (∀ ⦃x₁ : H⦄,
    x₁ ∈ t →
      ∀ ⦃y₁ : H⦄,
        y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔
  ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
Tactic: rw [isCornerFree_iff hAs, isCornerFree_iff this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (a, b, c) ∈ triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b
have simp : (∃ (a_1 : G) (b_1 : G), (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) ↔ (a, b) ∈ A ∧ c = a + b
Tactic: simp only [triangleIndices, Prod.ext_iff, mem_map, Embedding.coeFn_mk, Prod.exists,
    eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (∃ (a_1 : G) (b_1 : G), (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) ↔ (a, b) ∈ A ∧ c = a + b
have refine : (∃ (a_1 : G) (b_1 : G), (a_1, b_1) ∈ A ∧ a = a_1 ∧ b = b_1 ∧ c = a_1 + b_1) → (a, b) ∈ A ∧ c = a + b
Tactic: refine ⟨?_, fun h ↦ ⟨_, _, h.1, rfl, rfl, h.2⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ExplicitDisjoint (triangleIndices A)
have inj₀ : ∀ ⦃a b c a' : G⦄, (a, b, c) ∈ triangleIndices A → (a', b, c) ∈ triangleIndices A → a = a'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
inj₀ : ∀ ⦃a b c a' : G⦄, (a, b, c) ∈ triangleIndices A → (a', b, c) ∈ triangleIndices A → a = a'
⊢ ExplicitDisjoint (triangleIndices A)
have inj₁ : ∀ ⦃a b c b' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b', c) ∈ triangleIndices A → b = b'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
inj₀ : ∀ ⦃a b c a' : G⦄, (a, b, c) ∈ triangleIndices A → (a', b, c) ∈ triangleIndices A → a = a'
inj₁ : ∀ ⦃a b c b' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b', c) ∈ triangleIndices A → b = b'
⊢ ExplicitDisjoint (triangleIndices A)
have inj₂ : ∀ ⦃a b c c' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b, c') ∈ triangleIndices A → c = c'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (hypothesis)
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
hs : IsCornerFree (↑A : Set (G × G))
a a' b b' c c' : G
ha : (a', b, c) ∈ triangleIndices A
hb : (a, b', c) ∈ triangleIndices A
hc : (a, b, c') ∈ triangleIndices A
⊢ a = a' ∨ b = b' ∨ c = c'
have ha₁ : (a', b) ∈ A ∧ c = a' + b
Tactic: simp only [mk_mem_triangleIndices] at ha hb hc
Cleared hypotheses: ha, hb, hc