mathlib-initiative/mathlib-tactics huggingface dataset:
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
⊢ ∀ ⦃i₁ i₂ : ι''⦄ (f₁ : Y ⟶ X'' i₁) (f₂ : Y ⟶ X'' i₂) (hf₁ : f₁ ≫ f'' i₁ = s) (hf₂ : f₂ ≫ f'' i₂ = s),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₁)).op.toLoc (q' i₁).op.toLoc (r' i₁).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₁)))).hom ≫
        ((pullFunctor F ⋯).obj D).hom s f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w ⋙ pullFunctor F w').obj D).hom s f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₂)).op.toLoc (q' i₂).op.toLoc (r' i₂).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₂)))).hom

Tactic:
k₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ : ι''
⊢ ∀ ⦃i₂ : ι''⦄ (f₁ : Y ⟶ X'' k₁) (f₂ : Y ⟶ X'' i₂) (hf₁ : f₁ ≫ f'' k₁ = s) (hf₂ : f₂ ≫ f'' i₂ = s),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯)).symm.app
              (D.obj (α (β k₁)))).hom ≫
        ((pullFunctor F ⋯).obj D).hom s f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w ⋙ pullFunctor F w').obj D).hom s f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₂)).op.toLoc (q' i₂).op.toLoc (r' i₂).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₂)))).hom
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x✝ : α ⟶ S.obj (op PUnit.{u + 1})
⊢ eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝) = x✝

Tactic:
ext; simp [eval_typesGlue]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : G.obj X),
    {
          arrows := fun Y f ↦
            ∃ a, (ConcreteCategory.hom (G.map f.op)) x₂ = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
          downward_closed := ⋯ } =
        ⊤ →
      ∃ x₁, (ConcreteCategory.hom (m.app X)) x₁ = x₂

Tactic:
intro p hp

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
p : G.obj X
hp :
  { arrows := fun Y f ↦ ∃ a, (ConcreteCategory.hom (G.map f.op)) p = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
      downward_closed := ⋯ } =
    ⊤
⊢ ∃ x₁, (ConcreteCategory.hom (m.app X)) x₁ = p
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 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
this : e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)
⊢ χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
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₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : ψ = adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁
eq' : (Triangle.mk (G.map T.mor₁) f g).mor₁ ≫ (Triangle.mk (G.map T.mor₁) f g).mor₂ = 0
⊢ ψ ≫ f = 0

Tactic:
dsimp at eq eq'

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₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : ψ = adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁
eq' : G.map T.mor₁ ≫ f = 0
⊢ ψ ≫ f = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
m : (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj B)) ⟶ (Triangle.mk α β γ).obj₃
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = m ≫ (Triangle.mk α β γ).mor₃
⊢ (shiftFunctor C 1).map (ι.map k) = 0

Tactic:
obtain rfl : m = 0 := by
    rw [← cancel_epi ((shiftFunctorAdd' C (1 : ℤ) 1 2 (by lia)).hom.app _), comp_zero]
    exact eq_zero_of_hom_shift_pos hι _ (by lia)

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = 0 ≫ (Triangle.mk α β γ).mor₃
⊢ (shiftFunctor C 1).map (ι.map k) = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
m : (shiftFunctor C 1).obj (Triangle.mk α β γ).obj₁ ⟶ ι.obj B
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ m
⊢ k = 0

Tactic:
obtain rfl : m = 0 := by
    rw [← cancel_epi ((shiftFunctorAdd' C (1 : ℤ) 1 2 (by lia)).hom.app _), comp_zero]
    exact eq_zero_of_hom_shift_pos hι _ (by lia)

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ 0
⊢ k = 0
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ∅

Tactic:
exact threeGPFree_empty

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ↑∅

Tactic:
by norm_cast; exact threeGPFree_empty

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

Goal state before:
pp: n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i, x i ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
by
  rw [mem_box] at hx
  have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i =>
    Nat.pow_le_pow_left (Nat.le_sub_one_of_lt (hx i)) _
  exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [Finset.card_fin, smul_eq_mul])

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

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

Tactic:
← mul_one #((A / B) ×ˢ (C / B))

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

Tactic:
obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
⊢ CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(n / n.gcd (n / n.minFac)) ≤ ↑n.minFac

Tactic:
gcd_eq_right (div_dvd_of_dvd n.minFac_dvd),

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(n / (n / n.minFac)) ≤ ↑n.minFac
Module: Mathlib.Combinatorics.SimpleGraph.Dart

Goal state before:
pp: case mk
V : Type u_1
G : SimpleGraph V
d₂ : G.Dart
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝, adj := adj✝ } = d₂ ↔ { toProd := toProd✝, adj := adj✝ }.toProd = d₂.toProd

Tactic:
cases d₂

Goal state after:
case mk.mk
V : Type u_1
G : SimpleGraph V
toProd✝¹ : V × V
adj✝¹ : G.Adj toProd✝¹.1 toProd✝¹.2
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝¹, adj := adj✝¹ } = { toProd := toProd✝, adj := adj✝ } ↔
    { toProd := toProd✝¹, adj := adj✝¹ }.toProd = { toProd := toProd✝, adj := adj✝ }.toProd
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
⊢ v₂✝ ∈ u ↓∩ t → (SimpleGraph.induce u G).Adj v₁✝ v₂✝

Tactic:
ht

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
ht : v₂✝ ∈ u ↓∩ t
⊢ (SimpleGraph.induce u G).Adj v₁✝ v₂✝
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
⊢ (fun w ↦ w ≠ v ∧ Odd (G.degree w)) = fun w ↦ Odd (G.degree w) ∧ w ≠ v

Tactic:
ext w

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
w : V
⊢ w ≠ v ∧ Odd (G.degree w) ↔ Odd (G.degree w) ∧ w ≠ v
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1

Tactic:
hs hi hj

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Semiring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
s : Set α
hs : s.Subsingleton
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : Fintype ↑(H.neighborSet v)
h : Disjoint G H
⊢ Disjoint (G.neighborFinset v) (H.neighborFinset v)

Tactic:
simp [← Finset.disjoint_coe, disjoint_neighborSet.mpr h v]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
this : e.symm x✝ ≤ e.symm ⊥
⊢ x✝ ≤ ⊥

Tactic:
exact e.symm.map_rel_iff.mp this

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 : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #(G.edgeFinset ∩ s.sym2) = #(induce (↑s) G).edgeFinset

Tactic:
convert h.symm using 1

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)
⊢ #(induce (↑s) G).edgeFinset = #(induce (↑s) G).edgeFinset
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
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ b

Tactic:
Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)

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
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ d
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}

Tactic:
· exact hb

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ⊆ s.powerset

Tactic:
intro p hp

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ∈ s.powerset
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
⊢ IsIso (t.eTruncGEπ ⊥)

Tactic:
dsimp [eTruncGEπ]
  infer_instance

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ ({⊥} ∪ parts.erase ⊥).erase ⊥, f p = ∑ p ∈ {⊥} ∪ parts.erase ⊥, f p

Tactic:
sum_union_eq_right

Goal state after:
case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ ({⊥} ∪ parts.erase ⊥).erase ⊥, f p = ∑ a ∈ parts.erase ⊥, f a

case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∀ a ∈ {⊥}, a ∉ parts.erase ⊥ → f a = 0
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < ↑(initialBound ε l)

pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5

Tactic:
initialBound,

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < ↑(max 7 (max l (⌊log (100 / ε ^ 5) / log 4⌋₊ + 1)))

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: case inl
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 = ↑(#s)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
simpa [← hscard] using ht.trans sum_div_card_sq_le_sum_sq_div_card

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

Goal state before:
pp: case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
ht

Goal state after:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)
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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * 1 ≤ ↑(#s')
⊢ ↑(#t) * 1 ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1

Tactic:
ht

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * 1 ≤ ↑(#s')
ht : ↑(#t) * 1 ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

Tactic:
rw [hr]

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 1 - (1 - δ) * (1 - δ)