mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ (pullFunctor F ⋯).FullyFaithful

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F ⋯ ≅ F.toDescentData f')

Tactic:
· exact fullyFaithfulPullFunctor F hp h₁

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F ⋯ ≅ F.toDescentData f')
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S'✝ : SubmonoidFunctor M'
p : M ⟶ M'
S'' : SubmonoidFunctor M''
S' : SubmonoidFunctor M'
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : ↑(M.obj U✝)
h : x✝ ∈ Submonoid.comap (MonCat.Hom.hom (p.app U✝)) (S'.obj U✝)
⊢ x✝ ∈ Submonoid.comap (MonCat.Hom.hom (M.map x✝¹)) (Submonoid.comap (MonCat.Hom.hom (p.app V✝)) (S'.obj V✝))

Tactic:
simp_rw [Submonoid.mem_comap, NatTrans.naturality_apply]
    exact Submonoid.mem_comap.mp (Set.mem_of_mem_of_subset h (S'.map _))

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀} {χ' : G ⟶ e.functor.obj 𝒞₁.Ω},
    IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth) → χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
by
    intro χ₀' χ' hχ'
    have : e.inverse.map χ' ≫ e.unitInv.app _ = 𝒞₁.χ (e.inverse.map m) := by
      apply 𝒞₁.uniq (e.inverse.map m) (χ₀' := e.inverse.map χ₀' ≫ e.unitInv.app _)
      exact (hχ'.map e.inverse).paste_vert <| IsPullback.of_vert_isIso_mono .mk
    simpa using congr(e.counitInv.app G ≫ e.functor.map $this)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
⊢ φ ≫ G.map 0 ≫ (Functor.commShiftIso G 1).hom.app T.obj₂ = 0

Tactic:
G.map_zero,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
⊢ φ ≫ 0 ≫ (Functor.commShiftIso G 1).hom.app T.obj₂ = 0
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : Category.{v_2, u_2} D
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
E : C ≌ D
inst✝² : E.functor.CommShift ℤ
inst✝¹ : E.inverse.CommShift ℤ
inst✝ : E.CommShift ℤ
⊢ Equivalence.refl.IsTriangulated

Tactic:
dsimp [Equivalence.IsTriangulated]
  rw [refl_toAdjunction]
  infer_instance

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 12) ≤ log ↑N

Tactic:
exact log_le_log (by positivity) (mod_cast hN)

Goal state after:
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
⊢ (t.eTruncLT.obj ⊥).Additive

pp: case 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✝ : ℤ
⊢ (t.eTruncLT.obj (WithBotTop.coe a✝)).Additive

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
⊢ (t.eTruncLT.obj ⊤).Additive

Tactic:
all_goals dsimp; infer_instance

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
s x : G
⊢ A.convolution (B <• s)⁻¹⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)

Tactic:
inv_op_smul_finset_distrib,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (s⁻¹ •> B⁻¹)⁻¹ x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Fintype.card G.Dart = ∑ v, G.degree v

Tactic:
by
  have := Classical.decEq V
  simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]
  exact card_eq_sum_card_fiberwise (by simp)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (#{w | Odd (G.degree w)} - 1)

pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ {w | Odd (G.degree w)}

Tactic:
· refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
    lia

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
hc : (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ {w | Odd (G.degree w)}
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
⊢ G.minDegree ≤ (induce s G).minDegree

Tactic:
have := hs.to_subtype

Goal state after:
case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
⊢ G.minDegree ≤ (induce s G).minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.minDegree ≤ (induce s G).degree v

Tactic:
G.minDegree_le_degree v,

Goal state after:
case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.degree ↑v ≤ (induce s G).degree v
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.neighborSet ↑v ⊆ s

Tactic:
neighborSet_subset_support,

Goal state after:
case inr.inr
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
h✝ : Nonempty V
hs : s.Nonempty
this : Nonempty ↑s
v : ↑s
⊢ G.support ⊆ s
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≠ ⊥

Tactic:
by
  intro h
  refine P.bot_notMem (?_)
  rw [h] at hb
  exact hb

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
⊢ b ∈ P.parts

Tactic:
obtain ⟨c, hc, hbc⟩ := hQP hb

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
⊢ b ∈ P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
⊢ P ≤ (Finpartition.empty α).copy ⋯

pp: case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ indiscrete h

Tactic:
· intro x hx
      simpa [h, P.ne_bot hx] using P.le hx

Goal state after:
case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ indiscrete h
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
⊢ (t.eTruncGE.obj ⊥).Additive

pp: case 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✝ : ℤ
⊢ (t.eTruncGE.obj (WithBotTop.coe a✝)).Additive

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
⊢ (t.eTruncGE.obj ⊤).Additive

Tactic:
all_goals dsimp; infer_instance

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

Goal state before:
pp: case inr
α : 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)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #s

Tactic:
rw [← Nat.div_add_mod #s #P.parts]

Goal state after:
case inr
α : 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)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #P.parts * (#s / #P.parts) + #s % #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
⊢ ¬G.IsUniform ε s t ↔
    ∃ s' ⊆ s, ∃ t' ⊆ t, ↑(#s) * ε ≤ ↑(#s') ∧ ↑(#t) * ε ≤ ↑(#t') ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|

Tactic:
unfold IsUniform
  simp only [not_forall, not_lt, exists_prop, Rat.cast_abs, Rat.cast_sub]

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

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t

Tactic:
rw [← card_product, interedges_def, interedges_def]
  have : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2} := by
    refine filter_congr fun x hx ↦ ?_
    rw [mem_product] at hx
    rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
  rw [this, ← card_union_of_disjoint, filter_union_filter_not_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

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

Goal state before:
pp: case inr.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A / #P.parts + 1) ≤ ↑(#A) / ↑(#P.parts) + 1

Tactic:
simpa using Nat.cast_div_le

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

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
ε : 𝕜
hε : 0 < ε
P : Finpartition ⊥
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#⊥) ^ 2

pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
· simp [Subsingleton.elim P ⊥]

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ ε ^ 5 / 4 * (↑⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)

Tactic:
rwa [← Nat.cast_add_one]

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

Goal state before:
pp: ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
f : ι → G.Subgraph
⊢ (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Tactic:
by
  simp [iSup]

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)

Tactic:
ext <;> simp [Subgraph.map]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 V := hG'.some
he : e = hG'.some
⊢ False

Tactic:
have : e ∈ _ := hG'.some_mem

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 V := hG'.some
he : e = hG'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').edgeSet
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ G.singletonSubgraph v ≤ H ↔ v ∈ H.verts

Tactic:
refine ⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ v ∈ H.verts → G.singletonSubgraph v ≤ H
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
⊢ G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩

Goal state after:
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
⊢ (G'.coe.deleteEdges s).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v : V
hv : v ∈ (G'.deleteEdges s).verts
w : V
hw : w ∈ (G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)).Adj ⟨v, hv⟩ ⟨w, hw⟩
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case head
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h' }.edge ∈ G.edgeSet

Tactic:
exact h'

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
exact .inr (dart_fst_mem_support_of_mem_darts _ hd)

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

Goal state before:
pp: case cons.mp
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv

pp: case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil

Tactic:
· rintro ⟨_ | _, _, h⟩ <;> simp at h

Goal state after:
case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRec Hnil Hconcat (p.concat h) = Hconcat p h (concatRec Hnil Hconcat p)

Tactic:
simp only [concatRec]
  apply eq_of_heq (rec_heq_of_heq _ _)
  trans concatRecAux @Hnil @Hconcat (cons h.symm p.reverse)
  · congr
    simp
  · rw [concatRecAux, eqRec_heq_iff]
    congr <;> simp

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y ↦ (↑x ∩ ↑y).Subsingleton) (Finset.map f))

Tactic:
rintro s hs t ht hst

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ Function.onFun (fun x y ↦ (↑x ∩ ↑y).Subsingleton) (Finset.map f) s t
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
this : 2 ≤ 1
⊢ False

Tactic:
contradiction

Goal state after: