mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ (shiftFunctor C 1).obj (ι.obj K)
hm₃ : (shiftFunctor C 1).map m₃ = H.m₃
⊢ (shiftFunctor (Triangle C) 1).obj (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ∈ distinguishedTriangles

Tactic:
]

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ (shiftFunctor C 1).obj (ι.obj K)
hm₃ : (shiftFunctor C 1).map m₃ = H.m₃
⊢ (shiftFunctor (Triangle C) 1).obj (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ∈ distinguishedTriangles
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree t ↔ ThreeGPFree t

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a * f c = f b * f b

Tactic:
]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a * f c = f b * f b
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f b = f b

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b : α
hb : b = a ∨ b ∈ s
c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
⊢ b = c

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b : α
hb : b = a ∨ b ∈ s
c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
⊢ b = c
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : s.prod = t.prod
⊢ (map f₁ t).prod = (map f₁ t).prod

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ s.prod = t.prod ↔ s.prod = t.prod

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ↑(∑ b ∈ t, #(bipartiteBelow r s b)) = ↑(∑ x ∈ t, #(bipartiteBelow r s x))

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ #s • m = #s • m

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ b ∈ t, #(bipartiteBelow r s b) = ∑ x ∈ t, #(bipartiteBelow r s x)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ b ∈ t, #(bipartiteBelow r s b) = ∑ x ∈ t, #(bipartiteBelow r s x)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x ↦ a • x) b * (fun x ↦ a • x) d = (fun x ↦ a • x) c * (fun x ↦ a • x) c
⊢ b * d = c * c

Tactic:
by simpa [mul_mul_mul_comm _ _ a] using h

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a * a * (c * c) = a * a * (c * c)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s * 1 ≤ #t * 1

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s * 1 ≤ #t * 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
]

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ {b | b ∈ t ∧ r a b}.Nonempty

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ {b | b ∈ t ∧ r a b}.Nonempty
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a * c * (a * c) = a * c * (a * c)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ s.prod = t.prod ↔ s.prod = t.prod

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ t, (f ∘ g) x = id x

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ s, (f ∘ g) x = id x

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ t, (f ∘ g) x = id x

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ s, (f ∘ g) x = id x

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree {a}

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree {a}
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : #u = mulRothNumber (s ∪ t)
hu : ThreeGPFree ↑u
⊢ #u = #u

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
refine ⟨fun h' => ?_, hf.map_prod_eq_map_prod hsA htA hs ht⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
⊢ s.prod = t.prod
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ #(u ×ˢ v) ≤ mulRothNumber (s ×ˢ t)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ #(u ×ˢ v) ≤ mulRothNumber (s ×ˢ t)
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree (↑u ×ˢ ↑v)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree (↑u ×ˢ ↑v)
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
⊢ ¬n ≤ #t

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
⊢ ¬n ≤ #t
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ #(image (invFunOn f ↑A) s) ≤ mulRothNumber A

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ #(image (invFunOn f ↑A) s) ≤ mulRothNumber A
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ ThreeGPFree (invFunOn f ↑A '' ↑s)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ ThreeGPFree (invFunOn f ↑A '' ↑s)
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
⊢ mulRothNumber A ≤ mulRothNumber B
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → Finset β
h₁ : s.Nonempty
h₂ : ∀ j ∈ s, 0 < #(f j)
k : ℕ := s.inf' h₁ fun j ↦ #(f j)
hk : k = s.inf' h₁ fun j ↦ #(f j)
h₃ : ∀ a ∈ s, ∀ x ∈ f a, #{j | j ∈ s ∧ x ∈ f j} ≤ k
⊢ ∑ x ∈ s.biUnion f, #{j | j ∈ s ∧ x ∈ f j} = ∑ x ∈ s.biUnion f, #{j | j ∈ s ∧ x ∈ f j}

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝¹ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this✝ : s.prod = (map (g ∘ f) t).prod
this : s.prod = t.prod
⊢ s.prod = t.prod

pp: case g2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map (g ∘ f) t).prod
x : α
hx : x ∈ t
⊢ (g ∘ f) x = id x

pp: case g1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map (g ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝¹ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this✝ : s.prod = (map (g ∘ f) t).prod
this : s.prod = t.prod
⊢ s.prod = t.prod

case g2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map (g ∘ f) t).prod
x : α
hx : x ∈ t
⊢ (g ∘ f) x = id x

case g1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map (g ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ mulRothNumber A ≤ mulRothNumber B