mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: case h₂.h₁
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
X✝ Y✝ : (A ⊕ A') ⊕ T ⥤ B
f✝ : X✝ ⟶ Y✝
x✝ : A'
⊢ (((sum.associativity A A' T).congrLeft.trans
                      ((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor.map
                f✝ ≫
              ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                      isoWhiskerRight (sum.inlCompInverseAssociator A A' T) Y✝ ≪≫
                        (inl_ A A').associator (inl_ (A ⊕ A') T) Y✝).prod
                  (((inl_ A' T).isoWhiskerLeft
                          ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                        ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y✝).symm ≪≫
                          isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) Y✝ ≪≫
                            (inr_ A A').associator (inl_ (A ⊕ A') T) Y✝).prod
                    ((inr_ A' T).isoWhiskerLeft
                        ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                      ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y✝).symm ≪≫
                        isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) Y✝))).hom).2.1.app
      x✝ =
    (((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                      isoWhiskerRight (sum.inlCompInverseAssociator A A' T) X✝ ≪≫
                        (inl_ A A').associator (inl_ (A ⊕ A') T) X✝).prod
                  (((inl_ A' T).isoWhiskerLeft
                          ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                        ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X✝).symm ≪≫
                          isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) X✝ ≪≫
                            (inr_ A A').associator (inl_ (A ⊕ A') T) X✝).prod
                    ((inr_ A' T).isoWhiskerLeft
                        ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                      ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X✝).symm ≪≫
                        isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) X✝))).hom ≫
              (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans
                      (prod.associativity (A ⥤ B) (A' ⥤ B) (T ⥤ B))).functor.map
                f✝).2.1.app
      x✝

Tactic:
dsimp
        simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: case h₂
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
X✝ Y✝ : (A ⊕ A') ⊕ T ⥤ B
f✝ : X✝ ⟶ Y✝
x✝ : T
⊢ (((sum.associativity A A' T).congrLeft.trans
                      ((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor.map
                f✝ ≫
              ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                      isoWhiskerRight (sum.inlCompInverseAssociator A A' T) Y✝ ≪≫
                        (inl_ A A').associator (inl_ (A ⊕ A') T) Y✝).prod
                  (((inl_ A' T).isoWhiskerLeft
                          ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                        ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y✝).symm ≪≫
                          isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) Y✝ ≪≫
                            (inr_ A A').associator (inl_ (A ⊕ A') T) Y✝).prod
                    ((inr_ A' T).isoWhiskerLeft
                        ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                      ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y✝).symm ≪≫
                        isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) Y✝))).hom).2.2.app
      x✝ =
    (((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                      isoWhiskerRight (sum.inlCompInverseAssociator A A' T) X✝ ≪≫
                        (inl_ A A').associator (inl_ (A ⊕ A') T) X✝).prod
                  (((inl_ A' T).isoWhiskerLeft
                          ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                        ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X✝).symm ≪≫
                          isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) X✝ ≪≫
                            (inr_ A A').associator (inl_ (A ⊕ A') T) X✝).prod
                    ((inr_ A' T).isoWhiskerLeft
                        ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                      ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X✝).symm ≪≫
                        isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) X✝))).hom ≫
              (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans
                      (prod.associativity (A ⥤ B) (A' ⥤ B) (T ⥤ B))).functor.map
                f✝).2.2.app
      x✝

Tactic:
dsimp
        simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (ConcreteCategory.hom (S.toBiprod F n)) y =
    (ConcreteCategory.hom
        (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
      ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
        (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y)

Tactic:
apply (AddCommGrpCat.biprodIsoProd _ _).addCommGroupIsoToAddEquiv.injective
  dsimp [toBiprod]
  ext
  · rw [Iso.addCommGroupIsoToAddEquiv_apply,
      Iso.addCommGroupIsoToAddEquiv_apply,
      ← AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply,
      Iso.hom_inv_id_apply, ← ConcreteCategory.comp_apply,
      biprod.lift_fst, Iso.inv_hom_id_apply]
  · rw [Iso.addCommGroupIsoToAddEquiv_apply,
      Iso.addCommGroupIsoToAddEquiv_apply,
      ← AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply,
      Iso.hom_inv_id_apply, ← ConcreteCategory.comp_apply,
      biprod.lift_snd, Iso.inv_hom_id_apply]

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
⊢ ThreeGPFree (a • s)

Tactic:
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩ h

Goal state after:
α : 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
⊢ (fun x ↦ a • x) b = (fun x ↦ a • x) c
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
⊢ ThreeGPFree (a • s)

Tactic:
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩ h

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
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
⊢ (fun x ↦ a • x) b = (fun x ↦ a • x) 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 : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Finset α
hsA : ↑s ⊆ A
htA : ↑t ⊆ A
hs : s.card = n
ht : t.card = n
⊢ ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i ∈ s, f i = ∏ i ∈ t, f i

Tactic:
by
  simpa using hf.map_prod_eq_map_prod hsA htA hs ht

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

Goal state before:
pp: n d : ℕ
a : Fin (n + 1) → ℕ
⊢ (map d) a = a 0 + (∑ x, a x.succ * d ^ ↑x) * d

Tactic:
simp [map, Fin.sum_univ_succ, _root_.pow_succ, ← mul_assoc, ← sum_mul]

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

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

Tactic:
by
    rw [← map_map, ← map_map]
    rw [hg.map_prod_eq_map_prod _ _ (by rwa [card_map]) (by rwa [card_map]),
      hf.map_prod_eq_map_prod hsA htA hs ht]
    · simpa using fun a h ↦ hf.bijOn.mapsTo (hsA h)
    · simpa using fun a h ↦ hf.bijOn.mapsTo (htA h)

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

Goal state before:
pp: n d : ℕ
⊢ ∑ i, d * (2 * d + 1) ^ ↑i = ((2 * d + 1) ^ n - 1) / 2

Tactic:
refine (Nat.div_eq_of_eq_mul_left zero_lt_two ?_).symm

Goal state after:
n d : ℕ
⊢ (2 * d + 1) ^ n - 1 = (∑ i, d * (2 * d + 1) ^ ↑i) * 2
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
⊢ 2 ≠ 0

Tactic:
· exact two_ne_zero

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

Goal state before:
pp: case refine_1.refine_2
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b₁ : G
x✝¹ : b₁ ∈ ↑B
b₂ : G
x✝ : b₂ ∈ ↑B
h : (fun b ↦ (a / b, c / b)) b₁ = (fun b ↦ (a / b, c / b)) b₂
⊢ b₁ = b₂

Tactic:
· exact div_right_injective (Prod.ext_iff.1 h).1

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

Goal state before:
pp: case inr
N : ℕ
hN : N > 0
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
obtain h₁ | h₁ := le_or_gt 4096 N

Goal state after:
case inr.inl
N : ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

case inr.inr
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hts : #t < #s
⊢ #((t⁻¹, s⁻¹).1 * (t⁻¹, s⁻¹).2) = #((s, t).1 * (s, t).2) ∧
    #(t⁻¹, s⁻¹).1 + #(t⁻¹, s⁻¹).2 = #(s, t).1 + #(s, t).2 ∧ #(t⁻¹, s⁻¹).1 < #(s, t).1

Tactic:
simpa only [← mul_inv_rev, add_comm, card_inv, true_and]

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 ≤ #A

Tactic:
by
  rw [← inv_inv B, ← card_inter_smul]
  exact card_le_card inter_subset_left

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
⊢ #(x⁻¹ •> A ∩ B⁻¹) ≤ #B⁻¹

Tactic:
exact card_le_card inter_subset_right

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : ↑(G.neighborSet v)
h' : (v, ↑e₁) = (v, ↑e₂)
⊢ ↑e₁ = ↑e₂

Tactic:
convert! congr_arg Prod.snd h'

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : ↑(G.neighborSet v)
h : G.dartOfNeighborSet v e₁ = G.dartOfNeighborSet v e₂
⊢ ↑e₁ = ↑e₂

Tactic:
injection h with h'
    convert! congr_arg Prod.snd h'

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

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ b + 1 ≤ f y + 1

Tactic:
(hb y hy).1

Goal state after:
α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ f y + 1 ≤ f y + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.IsRegularOfDegree (Fintype.card V - 1)

Tactic:
simp [IsRegularOfDegree]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ G.minDegree = 0 ↔ G.support ≠ Set.univ

Tactic:
by
  simp [Set.ne_univ_iff_exists_notMem, minDegree_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
⊢ P = indiscrete ⋯

Tactic:
have h : ∀ b ∈ P.parts, b = a := fun _ hb ↦
      (ha.le_iff.mp <| P.le hb).resolve_left (P.ne_bot hb)

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
⊢ P = indiscrete ⋯
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:
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.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot.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
hab✝ : ⊥ ⟶ ⊥
hab : True
⊢ 𝟙 (𝟭 C) ≫ 0 = 0 ≫ Functor.whiskerRight (𝟙 0) (shiftFunctor C 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: case bot.coe
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
a✝ : ℤ
hab✝ : ⊥ ⟶ WithBotTop.coe a✝
hab : True
⊢ t.truncGEπ a✝ ≫ t.truncGEδLT a✝ = 0 ≫ Functor.whiskerRight 0 (shiftFunctor C 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: case bot.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
hab✝ : ⊥ ⟶ ⊤
hab : True
⊢ 0 ≫ 0 = 0 ≫ Functor.whiskerRight 0 (shiftFunctor C 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ P.parts, b ≤ c

Tactic:
by
      obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)
      rw [mem_product] at hc
      exact ⟨c.1, hc.1, inf_le_left⟩

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

Goal state before:
pp: case coe.coe
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
a✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : a✝¹ ≤ a✝
⊢ t.natTransTruncGEOfLE a✝¹ a✝ ⋯ ≫ t.truncGEδLT a✝ =
    t.truncGEδLT a✝¹ ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a✝¹ a✝ ⋯) (shiftFunctor C 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : True
⊢ 0 ≫ 0 = t.truncGEδLT a✝ ≫ Functor.whiskerRight (t.truncLTι a✝) (shiftFunctor C 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
y : Finset α
hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y
z : α
hz2 : z ∈ id y
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ y
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = y

Tactic:
obtain ⟨R, hR, rfl⟩ := hy

Goal state after:
α : 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.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
⊢ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id = t

Tactic:
by
  ext a
  refine mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ ?_⟩
  obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)
  refine ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ ?_, _, hau⟩, hau⟩
  obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2
  rw [mem_filter] at hau hb
  rwa [← hb.2 _ ht, hau.2 _ ht]

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

Goal state before:
pp: case pos
α : 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
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ a * m - m + b * (m + 1) = a * m + b * (m + 1) - m

Tactic:
refine ⟨m_pos, le_succ _, le_add_right (Nat.le_mul_of_pos_left _ ‹0 < a›), ?_⟩
      rw [tsub_add_eq_add_tsub (Nat.le_mul_of_pos_left _ h)]

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
ε : 𝕜
s : Finset α
h₁ : s ≠ s
h₂ : ¬G.IsUniform ε s s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2)
            (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) -
          G.edgeDensity s s|

Tactic:
cases h₁ rfl

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Tactic:
intro h' hs

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
h' : ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∈ s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} = ⨆ i, fromEdgeSet {↑i}

Tactic:
iSup,

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} = sSup (Set.range fun i ↦ fromEdgeSet {↑i})
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ List.count u (p.takeUntil u h).support = 1

Tactic:
by
  induction p
  · rw [mem_support_nil_iff] at h
    subst u
    simp
  · cases h
    · simp
    · simp! only
      split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.tail.darts = p.darts.tail

Tactic:
by
  simp [tail, darts_drop]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : ¬i ≤ p.length
⊢ i = 0

Tactic:
rw [p.getVert_of_length_le (le_of_not_ge h')] at h
    subst h
    simp_all

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

Goal state before:
pp: case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (insert a ↑s)

Tactic:
exact hs.1.insert fun b hb _ => h _ hb

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.reverse.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
← take_spec c h,

Goal state after:
case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.takeUntil w h).append (c.dropUntil w h)).reverse.IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ¬∀ (t : Finset α), ¬G.IsNClique n t
⊢ completeGraph (Fin n) ↪g G

Tactic:
push Not at h

Goal state after:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g G