mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ ∀ (E_1 : Multifork (F.multicospanIndex G)) (m : E_1.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E_1.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
intro t

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
⊢ ∀ (m : t.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫ F.p₂ p.snd =
    ((cylinderHom f g).comp g).h₀ p

Tactic:
have : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) (by simp) ≫
        pullback.snd (F.f _) (F.f _) := by simp
    dsimp only [cylinder_X, Hom.comp_s₀, cylinder_I₀, Function.comp_apply, cylinderHom_s₀,
      Hom.comp_h₀, cylinderHom_h₀]
    nth_rw 3 [this]
    rw [pullback.condition_assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X : Cᵒᵖ
⊢ ↾(J.overMapPullback A (𝟙 X).unop).map = 𝟙 ((J.overPullback A (unop X)).obj F ⟶ (J.overPullback A (unop X)).obj G)

Tactic:
ext φ : 4

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X : Cᵒᵖ
φ : (J.overPullback A (unop X)).obj F ⟶ (J.overPullback A (unop X)).obj G
⊢ ((ConcreteCategory.hom (↾(J.overMapPullback A (𝟙 X).unop).map)).toFun φ).hom =
    ((ConcreteCategory.hom (𝟙 ((J.overPullback A (unop X)).obj F ⟶ (J.overPullback A (unop X)).obj G))).toFun φ).hom
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾(J.overMapPullback A (f ≫ g).unop).map = ↾(J.overMapPullback A f.unop).map ≫ ↾(J.overMapPullback A g.unop).map

Tactic:
ext φ : 4

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
φ : (J.overPullback A (unop X✝)).obj F ⟶ (J.overPullback A (unop X✝)).obj G
⊢ ((ConcreteCategory.hom (↾(J.overMapPullback A (f ≫ g).unop).map)).toFun φ).hom =
    ((ConcreteCategory.hom (↾(J.overMapPullback A f.unop).map ≫ ↾(J.overMapPullback A g.unop).map)).toFun φ).hom
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ S ∈ ⊥ X

Tactic:
by
    obtain ⟨Y, a, ha, b, hb⟩ := hS ⟨_, ⟨X⟩⟩ (shrinkYonedaObjObjEquiv.symm (𝟙 X))
    obtain ⟨b, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective b
    dsimp at b hb
    have : b ≫ a = 𝟙 _ :=
      shrinkYonedaObjObjEquiv.symm.injective (by
        rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm])
    simpa only [bot_covering, ← Sieve.id_mem_iff_eq_top, this]
      using S.downward_closed ha b

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ P.triangEnvelopeIter n ≤ Q

Tactic:
rw [triangEnvelopeIter, retractClosure_le_iff]

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q
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
⊢ k ≫ ιK f₃ α = 0 → k = 0

Tactic:
hk

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 : k ≫ ιK f₃ α = 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
⊢ πQ f₂ β ≫ k = 0 → k = 0

Tactic:
hk

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 : πQ f₂ β ≫ k = 0
⊢ k = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: 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
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.triangleω₁δ a b c hab hbc).obj X ≅ (t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)

Tactic:
by
  refine Triangle.isoMk _ _ ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
    (t.eTruncLTGEIsoGELT a b).symm.app _) (Iso.refl _) ((t.eTruncGEIsoGEGE a b hab).app _) ?_ ?_ ?_
  · dsimp
    simp only [triangleω₁δ_obj_mor₁, homOfLE_leOfHom, Category.comp_id, Category.assoc]
    rw [← cancel_epi ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X)),
      ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp,
      ← cancel_epi ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X)),
      Iso.hom_inv_id_app_assoc, eTruncLTLTIsoLT_hom, eTruncLTLTToLT_app,
      ← Functor.map_comp, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app]
    simp
  · dsimp
    simp only [triangleω₁δ_obj_mor₂, eTruncGEToGEGE_app, Category.id_comp,
      ← t.eTruncGEπ_app_eTruncGE_map_app (homOfLE hab), ← NatTrans.naturality,
      eTruncGE_obj_map_eTruncGEπ_app]
  · simp [← Functor.map_comp_assoc, ← Functor.map_comp]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
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 (insert a s)

Tactic:
rintro ⟨hs, ha, ha'⟩ b hb c hc d hd h

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 ∈ insert a s
c : α
hc : c ∈ insert a s
d : α
hd : d ∈ insert a s
h : b * d = c * c
⊢ b = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
⊢ ∃ k ∈ range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))

Tactic:
refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_
  · rw [mem_range, Nat.lt_succ_iff]
    exact sum_sq_le_of_mem_box hx
  · rw [card_range, nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left₀, card_box]
    exact (cast_add_one_pos _).ne'

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

Goal state before:
pp: k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ ↑k
hu : u.card = m
⊢ ∀ x ∈ map val u, x ≤ k

Tactic:
simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))

Tactic:
convert! bound_aux' n d using 1
  rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow]
  rwa [cast_ne_zero]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
⊢ 1 ≤ K

Tactic:
grw [← hF]

Goal state after:
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
⊢ 1 ≤ ↑(#F)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) =
    ↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2)

Tactic:
hA.inv_eq_self,

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), f a b • (A * A ∩ (B⁻¹ * B)) =
    ↑(Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ A⁻¹ ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n

Tactic:
hA.inv_eq_self,

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ A ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A ^ 2)) * ↑(#(A ^ 3)) ≤ K * ↑(#A) * (K * ↑(#A))

Tactic:
gcongr
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i ∈ s, f i) / #s
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
simp_rw [← h]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i ∈ s, f i) / #s
⊢ ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ #⊤.edgeFinset = (Fintype.card V).choose 2

Tactic:
simp_rw [edgeFinset, Set.toFinset_card, edgeSet_top, ← Sym2.card_diagSet_compl]

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
apply le_minDegree_of_forall_le_degree
    exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

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

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ (SimpleGraph.map (⇑f) G).edgeFinset = map f.sym2Map G.edgeFinset

Tactic:
← Finset.coe_inj

Goal state after:
V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(SimpleGraph.map (⇑f) G).edgeFinset = ↑(map f.sym2Map G.edgeFinset)
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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ Disjoint ↑(id i) ↑(t.sup id)

Tactic:
sup_coe,

Goal state after:
α : 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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ Disjoint (↑(id i)) (t.sup fun x ↦ ↑(id x))

α : 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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ y₁ ≠ y₂

Tactic:
intro t

Goal state after:
case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
t : y₁ = y₂
⊢ False
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
i : EInt
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)

Tactic:
induction i using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
i : EInt
X : C
⊢ (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)

Tactic:
induction i using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
i : EInt
X : C
⊢ (t.eTriangleLTGE.obj i).obj X ∈ distinguishedTriangles

Tactic:
induction i using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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.IsLE X n
i : EInt
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
i : EInt
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
have : m * 4 ^ #P.parts ≤ card α / #P.parts := by
    rw [stepBound, ← Nat.div_div_eq_div_mul]
    exact Nat.div_mul_le_self _ _

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
n : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
n : ℤ
i : EInt
h : i ≤ WithBotTop.coe (n + 1)
X : C
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ Q
⊢ i ∈ R

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
⊢ i ∈ Q

Tactic:
· rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
⊢ i ∈ Q
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #(F.erase t).powerset ≤ 2 ^ (#F - 1)

Tactic:
card_powerset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ 2 ^ #(F.erase t) ≤ 2 ^ (#F - 1)