awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
rw : #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹
⊢ A.convolution B x ≤ #B

Tactic:
rw [← inv_inv B, ← inv_inv x, ← card_smul_inter, card_inv]

Premises used: Finset.card_inv, Finset.card_smul_inter, inv_inv
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹

Tactic:
card_le_card inter_subset_right

Premises used: Finset.inter_subset_right, Finset.card_le_card
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹

Tactic:
exact card_le_card inter_subset_right

Premises used: Finset.inter_subset_right, Finset.card_le_card
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
nth_rw : A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
⊢ A.convolution B x⁻¹ = B⁻¹.convolution A⁻¹ x

Tactic:
nth_rw 1 [← inv_inv B]

Premises used: inv_inv
-- Module: Mathlib.Combinatorics.Additive.Convolution
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)
rw₂ rw₃ : #(B⁻¹ ∩ x •> A) = #(B⁻¹ ∩ x •> A)
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x

Tactic:
rw [← card_smul_inter, ← card_inter_smul, inter_comm]

Premises used: Finset.inter_comm, Finset.card_smul_inter, Finset.card_inter_smul
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
nth_rw : #(A <• s ∩ x •> B⁻¹) = #(A ∩ x •> B⁻¹ <• s⁻¹)
⊢ (A <• s).convolution B x = A.convolution (s •> B) x

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]

Premises used: Finset.inv_smul_finset_distrib, inv_inv, Finset.card_inter_smul, HSMul.hSMul, SMulCommClass.smul_comm
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
⊢ #(A <• s ∩ x •> B⁻¹) = #(A ∩ x •> B⁻¹ <• s⁻¹)

Tactic:
simp [← card_smul_finset (op s) (A ∩ _), smul_finset_inter]

Premises used: Finset.smul_finset_inter, Inter.inter, Finset.card_smul_finset, MulOpposite.op
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
nth_rw : (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)⁻¹⁻¹
⊢ (s •> A).convolution B x = A.convolution B (s⁻¹ * x)

Tactic:
nth_rw 1 [← inv_inv x, ← inv_inv (s⁻¹ * x)]

Premises used: HMul.hMul, Inv.inv, inv_inv
-- Module: Mathlib.Combinatorics.Additive.Convolution
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⁻¹)
rw₅ rw₆ : #((x⁻¹ * s) •> A ∩ B⁻¹) = #((x⁻¹ * s) •> A ∩ B⁻¹)
⊢ (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]

Premises used: smul_smul, Finset.card_smul_inter, inv_inv, mul_inv_rev
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
s x : G
nth_rw : A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
⊢ A.convolution (B <• s) x = A.convolution B (x * s⁻¹)

Tactic:
nth_rw 2 [← inv_inv B]

Premises used: inv_inv
-- Module: Mathlib.Combinatorics.Additive.Convolution
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⁻¹)
rw₄ rw₅ : #(A ∩ (x * s⁻¹) •> B⁻¹) = #(A ∩ (x * s⁻¹) •> B⁻¹)
⊢ 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]

Premises used: Finset.inv_op_smul_finset_distrib, smul_smul, inv_inv, Finset.card_inter_smul, HSMul.hSMul, MulOpposite.op
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
inst_2 : Fintype G
B : Finset G
a : G
⊢ convolution univ B a = #B

Tactic:
simp [← card_inter_smul_inv]

Premises used: Finset.card_inter_smul_inv
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
inst_2 : Fintype G
A : Finset G
a : G
⊢ A.convolution univ a = #A

Tactic:
simp [← card_inter_smul_inv]

Premises used: Finset.card_inter_smul_inv
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
Goal:
G : Type u_1
inst : AddCommMonoid G
A B : Set (G × G)
hAB : A ⊆ B
hB : IsCornerFree B
⊢ IsCornerFree A

Tactic:
fun _x₁ _y₁ _x₂ _y₂ hxyd ↦ hB <| hxyd.mono hAB

Premises used: IsCorner.mono, IsCornerFree
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
Goal:
G : Type u_1
inst : AddCommMonoid G
x₁ y₁ x₂ y₂ : G
⊢ ¬IsCorner ∅ x₁ y₁ x₂ y₂

Tactic:
simp [isCorner_iff]

Premises used: isCorner_iff
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
Goal:
G : Type u_1
inst : AddCommMonoid G
A : Set (G × G)
hA : A.Subsingleton
_x₁ _y₁ _x₂ _y₂ : G
hxyd : IsCorner A _x₁ _y₁ _x₂ _y₂
⊢ _x₁ = _x₂

Tactic:
simpa using hA hxyd.fst_fst_mem hxyd.snd_fst_mem

Premises used: IsCorner.fst_fst_mem, IsCorner.snd_fst_mem
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
Goal:
G : Type u_1
inst : AddCommMonoid G
⊢ IsCornerFree.{u_1} (G := G) ∅

Tactic:
subsingleton_empty.isCornerFree

Premises used: Set.subsingleton_empty, Set.Subsingleton.isCornerFree
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
Goal:
G : Type u_1
inst : AddCommMonoid G
x : G × G
⊢ IsCornerFree (G := G) {x}

Tactic:
subsingleton_singleton.isCornerFree

Premises used: Set.subsingleton_singleton, Set.Subsingleton.isCornerFree
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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₂
⊢ (x₁, y₁) ∈ A

Tactic:
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
⊢ (x₁, y₂) ∈ A

Tactic:
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
⊢ (x₂, y₁) ∈ A

Tactic:
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
⊢ x₁ + y₂ = x₂ + y₁

Tactic:
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
hx₁y₁ : (x₁, y₁) ∈ A
hx₁y₂ : (x₁, y₂) ∈ A
hx₂y₁ : (x₂, y₁) ∈ A
hxy : x₁ + y₂ = x₂ + y₁
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Tactic:
⟨mem_image_of_mem _ hx₁y₁, mem_image_of_mem _ hx₁y₂, mem_image_of_mem _ hx₂y₁,
    hf.add_eq_add (hAs hx₁y₁).1 (hAs hx₁y₂).2 (hAs hx₂y₁).1 (hAs hx₁y₁).2 hxy⟩

Premises used: IsAddFreimanHom.add_eq_add, And.right, And.left, Set.mem_image_of_mem, IsCorner.mk
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
hx₁y₁ : (x₁, y₁) ∈ A
hx₁y₂ : (x₁, y₂) ∈ A
hx₂y₁ : (x₂, y₁) ∈ A
hxy : x₁ + y₂ = x₂ + y₁
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Tactic:
exact ⟨mem_image_of_mem _ hx₁y₁, mem_image_of_mem _ hx₁y₂, mem_image_of_mem _ hx₂y₁,
    hf.add_eq_add (hAs hx₁y₁).1 (hAs hx₁y₂).2 (hAs hx₂y₁).1 (hAs hx₁y₁).2 hxy⟩
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 : IsAddFreimanHom 2 s t f
hf' : InjOn f s
hAs : A ⊆ s ×ˢ s
hA : IsCornerFree (Prod.map f f '' A)
⊢ IsCornerFree A

Tactic:
fun _x₁ _y₁ _x₂ _y₂ hxy ↦
    hf' (hAs hxy.fst_fst_mem).1 (hAs hxy.snd_fst_mem).1 <| hA <| hxy.image hf hAs

Premises used: IsCorner.fst_fst_mem, IsCorner.image, IsCorner.snd_fst_mem, IsCornerFree, And.left
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
⊢ 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
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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)
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₁
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂

Tactic:
rw [isCorner_iff, isCorner_iff]

Premises used: isCorner_iff
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
a₃ : f x₁ + f y₂ = f x₂ + f y₁ ↔ x₁ + y₂ = x₂ + y₁
⊢ (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:
congr!
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 ↔ (x₁, y₁) ∈ A

Tactic:
hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₁)

Premises used: Set.Mem, Prod.map, Set.InjOn.mem_image_iff, Set.mk_mem_prod
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 ↔ (x₁, y₁) ∈ A

Tactic:
exact hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₁)

Premises used: Set.InjOn.mem_image_iff, Set.mk_mem_prod
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 ↔ (x₁, y₂) ∈ A

Tactic:
hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₂)

Premises used: Set.Mem, Prod.map, Set.InjOn.mem_image_iff, Set.mk_mem_prod
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 ↔ (x₁, y₂) ∈ A

Tactic:
exact hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₂)

Premises used: Set.InjOn.mem_image_iff, Set.mk_mem_prod
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 ↔ (x₂, y₁) ∈ A

Tactic:
hf'.mem_image_iff hAs (mk_mem_prod hx₂ hy₁)

Premises used: Set.Mem, Prod.map, Set.InjOn.mem_image_iff, Set.mk_mem_prod
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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 ↔ (x₂, y₁) ∈ A

Tactic:
exact hf'.mem_image_iff hAs (mk_mem_prod hx₂ hy₁)

Premises used: Set.InjOn.mem_image_iff, Set.mk_mem_prod
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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₂ = f x₂ + f y₁ ↔ x₁ + y₂ = x₂ + y₁

Tactic:
hf.add_eq_add hx₁ hy₂ hx₂ hy₁

Premises used: IsAddFreimanIso.add_eq_add
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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₂ = f x₂ + f y₁ ↔ x₁ + y₂ = x₂ + y₁

Tactic:
exact hf.add_eq_add hx₁ hy₂ hx₂ hy₁

Premises used: IsAddFreimanIso.add_eq_add
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
⊢ 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
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
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₂
⊢ IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A

Tactic:
rw [isCornerFree_iff hAs, isCornerFree_iff this]

Premises used: isCornerFree_iff
-- Module: Mathlib.Combinatorics.Additive.Corner.Defs
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
⊢ (∀ ⦃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:
simp +contextual only [hf.bijOn.forall, isCorner_image hf hAs, hf.bijOn.injOn.eq_iff]

Premises used: Set.InjOn.eq_iff, Set.BijOn.injOn, Set.BijOn.forall, IsAddFreimanIso.bijOn, isCorner_image
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A_1 : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
A : Finset (G × G)
x₁ x₂ : G
⊢ (x₁, x₂) = (x₁, x₂)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
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
⊢ (a, b, c) ∈ triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b

Tactic:
simp only [triangleIndices, Prod.ext_iff, mem_map, Embedding.coeFn_mk, Prod.exists,
    eq_comm]

Premises used: Prod.ext_iff, eq_comm, _private.0.Corners.triangleIndices, Function.Embedding.coeFn_mk, Finset.mem_map, Prod.exists
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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

Tactic:
⟨?_, fun h ↦ ⟨_, _, h.1, rfl, rfl, h.2⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
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
⊢ (∃ (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⟩⟩
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
h₁ : (a, b) ∈ A
h₂ : c = a + b
⊢ (a, b) ∈ A ∧ c = a + b

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
h₁ : (a, b) ∈ A
h₂ : c = a + b
⊢ (a, b) ∈ A ∧ c = a + b

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
⊢ #(triangleIndices A) = #A

Tactic:
card_map _

Premises used: Finset.card_map, _private.0.Corners.triangleIndices
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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'
inj₂ : ∀ ⦃a b c c' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b, c') ∈ triangleIndices A → c = c'
⊢ ExplicitDisjoint (triangleIndices A)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c a' : G⦄, (a, b, c) ∈ triangleIndices A → (a', b, c) ∈ triangleIndices A → a = a'

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c b' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b', c) ∈ triangleIndices A → b = b'

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
⊢ ∀ ⦃a b c c' : G⦄, (a, b, c) ∈ triangleIndices A → (a, b, c') ∈ triangleIndices A → c = c'

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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', b) ∈ A ∧ c = a' + b

Tactic:
simp only [mk_mem_triangleIndices] at ha hb hc

Premises used: _private.0.Corners.mk_mem_triangleIndices
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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
ha₁ : (a', b) ∈ A ∧ c = a' + b
⊢ (a, b') ∈ A ∧ c = a + b'

Tactic:
simp only [mk_mem_triangleIndices] at ha hb hc

Premises used: _private.0.Corners.mk_mem_triangleIndices
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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
ha₁ : (a', b) ∈ A ∧ c = a' + b
hb₁ : (a, b') ∈ A ∧ c = a + b'
⊢ (a, b) ∈ A ∧ c' = a + b

Tactic:
simp only [mk_mem_triangleIndices] at ha hb hc

Premises used: _private.0.Corners.mk_mem_triangleIndices
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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) ∈ A ∧ c = a' + b
hb : (a, b') ∈ A ∧ c = a + b'
hc : (a, b) ∈ A ∧ c' = a + b
⊢ a = a' ∨ b = b' ∨ c = c'

Tactic:
.inl <| hs ⟨hc.1, hb.1, ha.1, hb.2.symm.trans ha.2⟩

Premises used: And.right, And.left, Or.inl, Eq.symm, IsCorner.mk, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
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) ∈ A ∧ c = a' + b
hb : (a, b') ∈ A ∧ c = a + b'
hc : (a, b) ∈ A ∧ c' = a + b
⊢ a = a' ∨ b = b' ∨ c = c'

Tactic:
exact .inl <| hs ⟨hc.1, hb.1, ha.1, hb.2.symm.trans ha.2⟩

Premises used: And.right, And.left, Eq.symm, IsCorner.mk, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst_1 : Fintype G
inst_2 : DecidableEq G
hε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
⊢ (graph (triangleIndices A)).FarFromTriangleFree (ε / 9)

Tactic:
farFromTriangleFree _ ?_

Premises used: SimpleGraph.TripartiteFromTriangles.farFromTriangleFree
-- Module: Mathlib.Combinatorics.Additive.Corner.Roth
Goal:
G : Type u_1
inst : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst_1 : Fintype G
inst_2 : DecidableEq G
hε : ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card G) : ℝ) 2 ≤ (↑(#A) : ℝ)
refine :
  ε / 9 * (↑(HPow.hPow (β := ℕ) (Fintype.card G + Fintype.card G + Fintype.card G) 2) : ℝ) ≤
    (↑(#(triangleIndices A)) : ℝ)
⊢ (graph (triangleIndices A)).FarFromTriangleFree (ε / 9)

Tactic:
refine farFromTriangleFree _ ?_

Premises used: SimpleGraph.TripartiteFromTriangles.farFromTriangleFree