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✝³ : Preadditive C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
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
X Y : A
n : ℤ
f : (shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ (shiftEquiv C n).unitIso.hom.app (ι.obj X) ≫ (shiftFunctor C (-n)).map f =
    (shiftEquiv C n).unitIso.hom.app (ι.obj X) ≫ 0

Tactic:
comp_zero

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
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
X Y : A
n : ℤ
f : (shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ (shiftEquiv C n).unitIso.hom.app (ι.obj X) ≫ (shiftFunctor C (-n)).map f = 0
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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
⊢ (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) ≫ (shiftFunctor C 1).map (Triangle.mk α β γ).mor₁ = 0

Tactic:
by simp [← Functor.map_comp, hl]

Goal state after:
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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
m : (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj B)) ⟶ (Triangle.mk α β γ).obj₃
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = m ≫ (Triangle.mk α β γ).mor₃
⊢ (shiftFunctorAdd' C 1 1 2 mono_ιK._proof_1_4).hom.app (ι.obj B) ≫ m =
    (shiftFunctorAdd' C 1 1 2 mono_ιK._proof_1_4).hom.app (ι.obj B) ≫ 0

Tactic:
comp_zero

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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
m : (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj B)) ⟶ (Triangle.mk α β γ).obj₃
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = m ≫ (Triangle.mk α β γ).mor₃
⊢ (shiftFunctorAdd' C 1 1 2 mono_ιK._proof_1_4).hom.app (ι.obj B) ≫ m = 0
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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = (Triangle.mk (ι.map f₁) f₂ f₃).mor₃ ≫ 0
⊢ k = 0

Tactic:
comp_zero

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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
⊢ k = 0
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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
m : (shiftFunctor C 1).obj (Triangle.mk α β γ).obj₁ ⟶ ι.obj B
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ m
⊢ (shiftFunctorAdd' C 1 1 2 epi_πQ._proof_1_2).hom.app (ι.obj K) ≫ m =
    (shiftFunctorAdd' C 1 1 2 epi_πQ._proof_1_2).hom.app (ι.obj K) ≫ 0

Tactic:
comp_zero

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
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
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
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
m : (shiftFunctor C 1).obj (Triangle.mk α β γ).obj₁ ⟶ ι.obj B
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ m
⊢ (shiftFunctorAdd' C 1 1 2 epi_πQ._proof_1_2).hom.app (ι.obj K) ≫ m = 0
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
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
hT' : Triangle.mk (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))) 0 0 ∈ distinguishedTriangles
⊢ KernelFork.ofι
      (ιK (-(shiftFunctor C 1).map (Triangle.mk (ι.map f₁) (ι.map f₂) f₃).mor₁) (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))))
      ⋯ ≅
    KernelFork.ofι f₁ ⋯

Tactic:
exact Fork.ext (-(Iso.refl _)) ((ι ⋙ shiftFunctor C (1 : ℤ)).map_injective
    (by simp))

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
c : α
hc : c ∈ s
hb : a ∈ s
habc : a * c = a * a
⊢ a = c

Tactic:
simpa using habc.symm

Goal state after:
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
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
have := (hf.subset hsA hfs.bijOn_image).threeGPFree_congr.1 hs

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 (f '' ↑s)
⊢ mulRothNumber A ≤ mulRothNumber B
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ ‖toLp 2 (Nat.cast ∘ x)‖ = √↑k

Tactic:
rw [EuclideanSpace.norm_eq]

Goal state after:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i, ‖(toLp 2 (Nat.cast ∘ x)).ofLp i‖ ^ 2) = √↑k
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ i, |↑(x i)| ^ 2) = √↑k

Tactic:
simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]

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

Goal state before:
pp: ⊢ 2 ≤ 8 - 8 * 2 / rexp 1

pp: ⊢ 0 < 1 - 2 / rexp 1

Tactic:
le_sub_comm,

Goal state after:
⊢ 8 * 2 / rexp 1 ≤ 8 - 2

⊢ 0 < 1 - 2 / rexp 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ x / rexp 1 ≤ x / 2 - 1

Tactic:
le_sub_comm,

Goal state after:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 1 ≤ x / 2 - x / rexp 1
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B / A) * #(B * C)

Tactic:
by
  simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_invMul_mul_mul A⁻¹ B C

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 * 1 ∈ ↑A * ↑A

Tactic:
exact Set.mul_mem_mul hA₁ hA₁

Goal state after:
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
⊢ minOrder G = ⊤

Tactic:
by
  simpa [minOrder] using fun _ ↦ not_isOfFinOrder_of_isMulTorsionFree

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≤ #B

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

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≤ #B

Tactic:
by
  rw [← inv_inv B, ← inv_inv x, ← card_smul_inter, card_inv]
  exact card_le_card inter_subset_right

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ s(f a, f b) = s(x✝, y✝)

Tactic:
ha,

Goal state after:
case right
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ s(x✝, f b) = s(x✝, y✝)
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case inr
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
intro hs

Goal state after:
case inr
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1

Tactic:
rw [hs hi hj]
  exact le_add_of_nonneg_right zero_le_one

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb
      obtain ⟨d, hd, hcd⟩ := hQR hc
      exact ⟨d, hd, hbc.trans hcd⟩

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
⊢ Disjoint (id i) (t.sup id)

Tactic:
classical
      have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
      rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]
      · apply P.supIndep
        · simpa [image_subset_iff_subset_preimage] using ht
        · simpa using hi
        · simpa [i.property] using hi'
      exact Prsup

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
heq : (image (fun x ↦ x ⊓ b) P.parts).erase ⊥ = image (fun x ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥})
⊢ ∑ p ∈ (P.restrict hb).parts, f p = ∑ q ∈ P.parts, f (q ⊓ b)

Tactic:
have hz : ∑ x ∈ P.parts.filter (¬ · ⊓ b ≠ ⊥), f (x ⊓ b) = 0 := Finset.sum_eq_zero fun x hx => by
    simp only [ne_eq, Decidable.not_not, Finset.mem_filter] at hx
    rw [hx.2, hf]

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
heq : (image (fun x ↦ x ⊓ b) P.parts).erase ⊥ = image (fun x ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥})
hz : ∑ x ∈ P.parts with ¬x ⊓ b ≠ ⊥, f (x ⊓ b) = 0
⊢ ∑ p ∈ (P.restrict hb).parts, f p = ∑ q ∈ P.parts, f (q ⊓ b)
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
⊢ ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts

Tactic:
let z := fun a ↦ #P.parts * (f a).2 + g (f a).1

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
⊢ ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case top
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE ((t.eTruncGE.obj ⊤).obj X) n

Tactic:
exact isGE_of_isZero _ (by simp) _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max ↑7 ↑(max l (⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5

Tactic:
Nat.cast_max

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE ((t.eTruncLT.obj ⊥).obj X) n

Tactic:
exact isGE_of_isZero _ (by simp) _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
replace ht : ε ≤ 0 := by simpa using ht
    exact (hε.not_ge ht).elim

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ P.IsUniform G 1

Tactic:
rw [IsUniform, mul_one, Nat.cast_le]

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #(P.nonUniforms G 1) ≤ #P.parts * (#P.parts - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∑ A ∈ P.parts.attach,
      #(if hUcard : #↑A = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
          else equitabilise ⋯).parts =
    stepBound #P.parts

Tactic:
apply_dite Finpartition.parts,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∑ x ∈ P.parts.attach,
      #(if h : #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then (equitabilise ⋯).parts
        else (equitabilise ⋯).parts) =
    stepBound #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ ∀ x ∈ insert u (P.parts.erase u), #(x \ {y ∈ (R.extend ⋯ ⋯ ⋯).parts | y ⊆ x}.biUnion id) ≤ m

Tactic:
simp only [mem_insert, forall_eq_or_imp, extend_parts]

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m ∧
    ∀ a ∈ P.parts.erase u, #(a \ {y ∈ insert t R.parts | y ⊆ a}.biUnion id) ≤ m