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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ pullHom (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) g₁ Z.hom Z.hom ⋯ ⋯ =
    pullHom (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) ⋯) g₂ Z.hom Z.hom ⋯ ⋯

Tactic:
rw [familyOfElements_eq _ _ _ _ fac₁, familyOfElements_eq _ _ _ _ fac₂,
    ← dsimp% mor_precomp w φ Y₁.hom a₁ fac₁ _ _ _ hg₁ rfl,
    ← dsimp% mor_precomp w φ Y₂.hom a₂ fac₂ _ _ _ hg₂ rfl]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ mor w φ Z.hom (g₁ ≫ a₁) ⋯ = mor w φ Z.hom (g₂ ≫ a₂) ⋯
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := ⋯
t : (X : C) → ι X → F.obj (Opposite.op X) := ⋯
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ some ↑x = some ↑y

Tactic:
simp [← hi _ x.prop, ← hi _ y.prop, hxy]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝ : Epi ((presheafToSheaf J D).map f.hom)
this : Epi ((presheafToSheaf J D).map i)
⊢ IsRegularEpi f

Tactic:
have : IsIso ((presheafToSheaf J D).map i) :=
      Balanced.isIso_of_mono_of_epi _

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsRegularEpi f
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
⊢ (𝟭 (Sheaf typesGrothendieckTopology (Type u))).map f ≫ (equivYoneda' S₂).hom =
    (equivYoneda' S₁).hom ≫
      ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙ (evaluation Type uᵒᵖ (Type u)).obj (op PUnit.{u + 1})) ⋙
            yoneda').map
        f

Tactic:
by
        ext ⟨α⟩ s
        dsimp at s ⊢
        ext x
        exact eval_app S₁ S₂ f α s x

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
⊢ F.IsStackFor (Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence

Tactic:
by
  simp only [isStackFor_iff]
  apply DescentData.isEquivalence_toDescentData_iff_of_sieve_eq
  rw [Sieve.ofArrows_category']

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ Ω₀} {χ' : G ⟶ Ω}, IsPullback m χ₀' χ' t → χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
intro χ₀' χ' hχ'
    have : χ' ≫ eΩ.inv = 𝒞.χ m := by
      apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)
      exact hχ'.paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))
    simpa using this =≫ eΩ.hom

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) (χ m) (truth C)

Tactic:
by
  refine IsPullback.of_forall_isPullback_app fun X => ?_
  rw [Types.isPullback_iff]
  refine ⟨congr(($(comp_χ_eq m)).app X), ?_, ?_⟩
  · simpa using! (mono_iff_injective (m.app X)).mp (inferInstance)
  · simp only [Functor.const_obj_obj, Functor.sieves_obj, χ_app, Opposite.op_unop,
      TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, truth_app, Functor.isTerminalConst_from_app,
      Types.isTerminalPUnit_from_apply, and_true, forall_const]
    intro p hp
    simpa [eq_comm] using! congr($(hp).arrows (𝟙 _))

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ ((ConcreteCategory.hom (χ'.app X)).toFun x).arrows f ↔
    ((ConcreteCategory.hom
              (↾fun x ↦
                {
                  arrows := fun Y f ↦
                    ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                  downward_closed := ⋯ })).toFun
          x).arrows
      f

Tactic:
rw [Sieve.mem_iff_pullback_eq_top, ← Quiver.Hom.unop_op f]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ Sieve.pullback f.op.unop ((ConcreteCategory.hom (χ'.app X)).toFun x) = ⊤ ↔
    ((ConcreteCategory.hom
              (↾fun x ↦
                {
                  arrows := fun Y f ↦
                    ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                  downward_closed := ⋯ })).toFun
          x).arrows
      f.op.unop
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
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
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
⊢ WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y

Tactic:
induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f)
      | top => exact t.truncLTι a

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (sphere x r)

Tactic:
convert! threeAPFree_frontier isClosed_closedBall (strictConvex_closedBall ℝ x r)
    exact (frontier_closedBall _ hr).symm

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

Goal state before:
pp: case e'_2.e'_5
a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)

Tactic:
exact (add_tsub_cancel_of_le h).symm

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 = ↑d ^ n / (↑(d ^ 2) * ↑n)

Tactic:
← div_div,

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n = ↑d ^ n / ↑(d ^ 2) / ↑n
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / (√(log ↑N) * 1.38)

Tactic:
← div_div,

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / √(log ↑N) / 1.38
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
div_inv_eq_mul

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B⁻¹ ≤ #(A * B⁻¹) * #(B⁻¹ * C)
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s).Finite
⊢ n ≤ ↑(Nat.card ↥s)

pp: case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
a : G
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ ↑(orderOf a)

Tactic:
· obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs
    exact
      (h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
        (WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
a : G
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ ↑(orderOf a)
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
⊢ ↑p.minFac = ↑p

Tactic:
hp.minFac_eq

Goal state after:
p : ℕ
hp : Nat.Prime p
⊢ ↑p = ↑p
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:

Tactic:
(#(A ^ m) : ℝ) = #((finRange m).map fun i ↦ A ^ 1).prod := by simp
    _ ≤ K ^ (m - 2) * #A :=
      inductive_claim_mul hm (fun δ hδ ↦ by simpa [this _ (hδ _), pow_succ'] using hA) _ (by simp)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d d' : G.Dart
⊢ d' ∈ {d' | d'.edge = d.edge} ↔ d' ∈ {d, d.symm}

Tactic:
simpa using dart_edge_eq_iff d' d

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

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
· simpa [hvw, not_iff_not] using f.map_adj_iff (v := v) (w := w)

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G ≃g G'
⊢ ⇑f '' ⇑f.toEmbedding ⁻¹' G'.neighborSet (f.toEmbedding v) = G'.neighborSet (f v)

Tactic:
apply Equiv.image_preimage

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

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

Tactic:
h _ ha,

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

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ (induce s G).degree v = G.degree ↑v

Tactic:
simp_rw [← card_neighborFinset_eq_degree,
    ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(map (Embedding.subtype fun x ↦ x ∈ ↑s).sym2Map (induce (↑s) G).edgeFinset) = #(G.edgeFinset ∩ (↑s).toFinset.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset

Tactic:
rw [card_map, toFinset_coe] at h

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this✝ : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b a

Tactic:
grw [← P.sup_parts, this]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this✝ : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b ((Q.parts.erase b).sup id)
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
X : C
⊢ (t.eTruncLT.obj ⊥).map ((t.eTruncLTι ⊥).app X) = (t.eTruncLTι ⊥).app ((t.eTruncLT.obj ⊥).obj X)

Tactic:
simp [truncLT_map_truncLTι_app]

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

Goal state before:
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
X : C
a✝ : ℤ
⊢ (t.eTruncLT.obj (WithBotTop.coe a✝)).map ((t.eTruncLTι (WithBotTop.coe a✝)).app X) =
    (t.eTruncLTι (WithBotTop.coe a✝)).app ((t.eTruncLT.obj (WithBotTop.coe a✝)).obj X)

Tactic:
simp [truncLT_map_truncLTι_app]

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

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

Tactic:
simp [truncLT_map_truncLTι_app]

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:
by
  induction i using WithBotTop.rec with simp [truncGE_map_truncGEπ_app]

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
i : EInt
X : C
f : i ⟶ ⊥
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (f ≫ homOfLE ⋯)).app ((t.eTruncLT.obj ⊥).obj X)

Tactic:
simp [truncLT_map_truncLTι_app]

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

Goal state before:
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
i : EInt
X : C
a✝ : ℤ
f : i ⟶ WithBotTop.coe a✝
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (f ≫ homOfLE ⋯)).app ((t.eTruncLT.obj (WithBotTop.coe a✝)).obj X)

Tactic:
simp [truncLT_map_truncLTι_app]

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

Goal state before:
pp: case top
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i : EInt
X : C
f : i ⟶ ⊤
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (f ≫ homOfLE ⋯)).app ((t.eTruncLT.obj ⊤).obj X)

Tactic:
simp [truncLT_map_truncLTι_app]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
rw [bind_parts, mem_biUnion]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
⊢ ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)

Tactic:
simp +contextual [← Quotient.eq]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 1 - edgeDensity (fun x y ↦ ¬r x y) s₁ t₁ -
      (edgeDensity r s₂ t₂ + edgeDensity (fun x y ↦ ¬r x y) s₂ t₂ - edgeDensity (fun x y ↦ ¬r x y) s₂ t₂) ≤
    1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Tactic:
edgeDensity_add_edgeDensity_compl _ hs₂ ht₂,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 1 - edgeDensity (fun x y ↦ ¬r x y) s₁ t₁ - (1 - edgeDensity (fun x y ↦ ¬r x y) s₂ t₂) ≤
    1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

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

Tactic:
Nat.cast_le

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

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

Tactic:
by
  rw [IsUniform, mul_one, Nat.cast_le]
  refine (card_filter_le _
    (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans ?_
  rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]

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

Goal state before:
pp: case a.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∀ (a b : Finset α), a ∈ P.parts → b ∈ P.parts → a ≠ b → #a * #b ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

Tactic:
rintro U V hU hV -

Goal state after:
case a.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ ↑(#U * #V) ≤ ↑((#A / #P.parts + 1) * (#A / #P.parts + 1))

Tactic:
Nat.cast_le

Goal state after:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

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

Tactic:
ext <;> simp [Set.image_union, map_adj, sup_adj, Relation.Map, or_and_right, exists_or]

Goal state after: