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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₁.op))
        ((ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
          (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))))) =
    (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₂.op))
        ((ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
          (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))))

Tactic:
← comp_apply,

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom ((S.map (↾fun x ↦ PUnit.unit).op ≫ S.map g₁.op) ≫ S.map g.op))
      (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))) =
    (ConcreteCategory.hom ((S.map (↾fun x ↦ PUnit.unit).op ≫ S.map g₂.op) ≫ S.map g.op))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom
        (↾fun x ↦ (ConcreteCategory.hom (S.map (↾fun x_1 ↦ x).op)) ((ConcreteCategory.hom (S.map f.op)) s)))
      x =
    (ConcreteCategory.hom (↾fun x ↦ (ConcreteCategory.hom (S.map (↾fun x_1 ↦ x).op)) s)) ((ConcreteCategory.hom f) x)

Tactic:
← comp_apply,

Goal state after:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (↾fun x ↦ (ConcreteCategory.hom (S.map f.op ≫ S.map (↾fun x_1 ↦ x).op)) s)) x =
    (ConcreteCategory.hom (f ≫ ↾fun x ↦ (ConcreteCategory.hom (S.map (↾fun x_1 ↦ x).op)) s)) x
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left ((h.iso m).inv.hom ≫ (h.iso m).hom.hom) ≫ pullbackπ (h.χ m) h.Ω₀ = pullbackπ (h.χ m) h.Ω₀

Tactic:
convert! Category.id_comp _ using 2

Goal state after:
case e'_2.e'_6
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left ((h.iso m).inv.hom ≫ (h.iso m).hom.hom) =
    𝟙 (representative.obj ((Subobject.pullback (h.χ m)).obj h.Ω₀)).obj.left
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
⊢ P.triangEnvelope ≤ Q

Tactic:
triangEnvelope,

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.triangEnvelopeIter n ≤ Q
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₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
⊢ ψ ≫ g - ψ ≫ ((adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃) ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = 0

Tactic:
sub_eq_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₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
⊢ ψ ≫ g = ψ ≫ ((adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃) ≫ (Functor.commShiftIso G 1).hom.app T.obj₁
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
⊢ IsLimit (KernelFork.ofι f₁ ⋯)

Tactic:
have hT' : Triangle.mk (𝟙 ((ι.obj X₁)⟦(1 : ℤ)⟧)) (0 : _ ⟶ ι.obj 0) 0 ∈ distTriang C := by
    refine isomorphic_distinguished _ (contractible_distinguished
      (((ι ⋙ shiftFunctor C (1 : ℤ)).obj X₁))) _ ?_
    exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (IsZero.iso (by
      dsimp
      rw [IsZero.iff_id_eq_zero, ← ι.map_id, id_zero, ι.map_zero]) (isZero_zero C))

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
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
⊢ IsLimit (KernelFork.ofι f₁ ⋯)
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✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
⊢ ∃ X₁ i δ, Triangle.mk (ι.map i) (ι.map π) δ ∈ distinguishedTriangles

Tactic:
by
  obtain ⟨X₁, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map π)
  have : admissibleMorphism ι π := by simp [hA]
  obtain ⟨K, Q, α, β, γ, hT'⟩ := this f₂ f₃ hT
  have hQ : 𝟙 Q = 0 :=
    Cofork.IsColimit.hom_ext (isColimitCokernelCofork hι hT hT') (by
      dsimp
      rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β])
  have : IsIso α := (Triangle.isZero₃_iff_isIso₁ _ hT').1 (by
    dsimp
    rw [IsZero.iff_id_eq_zero, ← ι.map_id, hQ, ι.map_zero])
  refine ⟨K, -ιK f₃ α, f₂ ≫ inv α, ?_⟩
  rw [rotate_distinguished_triangle]
  refine isomorphic_distinguished _ hT _ ?_
  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (asIso α)

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

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

Tactic:
(mem_filter.1 hx).2

Goal state after:
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:
by
  rw [EuclideanSpace.norm_eq]
  dsimp
  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: n d k : ℕ
x : Fin n → ℕ
hx : x ∈ ↑(sphere n d k)
⊢ x ∈ (fun x ↦ toLp 2 (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 √↑k

Tactic:
rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]

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

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2

pp: case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12

Tactic:
· exact log_two_gt_d9.le.trans' (by norm_num1)

Goal state after:
case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
⊢ {x} * A' * B ⊆ C * A * B

Tactic:
rw [h₀]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
⊢ {x} * A ∩ (C * A) * B ⊆ C * A * B
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A ^ 0)) ≤ K ^ (0 - 1) * ↑(#A)

Tactic:
by simpa using hA.nonempty

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)

Tactic:
rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.minDegree = Fintype.card V - 1

Tactic:
by
  cases isEmpty_or_nonempty V
  · simp
  exact IsRegularOfDegree.top.minDegree_eq

Goal state after:
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
⊢ G.minDegree ≤ (induce s G).minDegree

Tactic:
refine le_minDegree_of_forall_le_degree _ _ fun 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.minDegree ≤ (induce s G).degree v
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (P.parts.sup fun x ↦ x) = a

Tactic:
← Function.id_def,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ P.parts.sup id = a
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ (P.parts.sup fun x ↦ x) \ b = a \ b

Tactic:
← Function.id_def,

Goal state after:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ P.parts.sup id \ b = a \ b
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b✝ c : α
P : Finpartition a
b : α
⊢ (image (fun x ↦ x \ b) P.parts).sup id = a \ b

Tactic:
by rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a : α
P : Finpartition a
⊢ (P.extendOfLE ⋯).parts = P.parts

Tactic:
simp [extendOfLE]

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
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A) * (↑(#A) / ↑(#P.parts) + 1) = ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
← div_add_same (mod_cast h.card_pos.ne'),

Goal state after:
α : 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) * ((↑(#A) + ↑(#P.parts)) / ↑(#P.parts)) = ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)
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
⊢ Nonempty α

Tactic:
← Fintype.card_pos_iff

Goal state after:
α : 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
⊢ 0 < Fintype.card α
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
⊢ G.deleteEdges s = G

Tactic:
by ext u v; simpa using (·.ne <| hs ·)

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
· rw [hr.1, hr.2, Subgraph.adj_comm]

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

Goal state before:
pp: case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * ↑(#P.parts) ^ 2 ≤ ↑(#P.parts.offDiag) * 7

Tactic:
offDiag_card

Goal state after:
case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * ↑(#P.parts) ^ 2 ≤ ↑(#P.parts * #P.parts - #P.parts) * 7
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝² : Fintype V
inst✝¹ : Fintype W
inst✝ : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ G.labelledCopyCount H = 1

Tactic:
by
  convert! Fintype.card_unique
  exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ {G' | Nonempty (⊥ ≃g G'.coe)} = {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}

Tactic:
simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]

Goal state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ Nonempty (⊥ ≃g { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe) ∧
    ∀ (x : G.Subgraph) (a : ⊥ ≃g x.coe), x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
⊢ G.killCopies ⊥ = G

Tactic:
by
  rw [killCopies]; exact dif_pos rfl

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

Goal state before:
pp: case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil

Tactic:
· rintro ⟨rfl, _, _⟩
      simp

Goal state after:
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
⊢ (p.takeUntil u h).append (p.dropUntil u h) = p

Tactic:
induction p
  · rw [mem_support_nil_iff] at h
    subst u
    rfl
  · cases h
    · simp!
    · simp! only
      split_ifs with h' <;> subst_vars <;> simp [*]

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.support.dropLast ++ [v] = p.support

Tactic:
cases p with | nil => rfl | cons h p

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).support.dropLast ++ [v] = (cons h p).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ p.take n = p.copy ⋯ ⋯

Tactic:
by
  induction n generalizing p u with
  | zero => cases p <;> simp [take] at h ⊢
  | succ n ih =>
    cases p
    · simp [take]
    rw [length_cons, Nat.add_le_add_iff_right] at h
    simp [take, ih h]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.tail.support ~ p.dropLast.support

Tactic:
cases p with | nil => rfl | cons h p

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).tail.support ~ (cons h p).dropLast.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.tail ~ p.support.dropLast

Tactic:
cases p with | nil => rfl | cons h p

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).support.tail ~ (cons h p).support.dropLast
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : f.topEmbedding w✝¹ ≠ f w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f w✝)

Tactic:
← Copy.topEmbedding_apply

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : f.topEmbedding w✝¹ ≠ f.topEmbedding w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ p.length - 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp; lia

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : 2 ≤ n
⊢ ⊥.CliqueFree n

Tactic:
intro t ht
  have := le_trans h (isNClique_bot_iff.1 ht).1
  contradiction

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

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : v ≠ w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Tactic:
rw [← top_adj, ← f.topEmbedding.map_adj_iff, comap_adj, top_adj] at hn

Goal state after:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : (f.topEmbedding v).fst ≠ (f.topEmbedding w).fst
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
⊢ (Walk.map f p).IsTrail ↔ p.IsTrail

Tactic:
by
  rw [isTrail_def, isTrail_def, edges_map, List.nodup_map_iff <| Sym2.map.injective hinj]

Goal state after: