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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (op 0))

Tactic:
by
  simp_rw [← Sheaf.isLocallySurjective_iff_epi'] at hF ⊢
  exact isLocallySurjective_π_app_zero_of_isLocallySurjective_map hc hF h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
Y : C
i : (cylinder f g).I₀
⊢ (F.sieve₁' (f.s₀ i.fst) (g.s₀ i.fst)).arrows
    (pullback.snd (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd) ≫ F.toPullback i.snd)

Tactic:
exact Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ _) _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ 𝟙 (F.obj (op Y)) ≫ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    (F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left)))) ≫ G.map (Over.Hom.left f).op

Tactic:
rw [id_comp, assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
⊢ Function.Bijective (S.toPullbackObj P)

Tactic:
rwa [← sheafCondition_iff_bijective_toPullbackObj]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F' R

Tactic:
rw [← Presieve.isSheafFor_iff_of_nat_equiv e he]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: case restrict
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) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
Z✝ W✝ : C
f : Z✝ ⟶ W✝
a✝ : F.obj (Opposite.op W✝)
ha : K.SubsheafClosure 𝒮 W✝ a✝
ih : ∃ i, Witness.eval hF ι t i = some a✝
⊢ ∃ i, Witness.eval hF ι t i = some ((ConcreteCategory.hom (F.map f.op)) a✝)

Tactic:
obtain ⟨i, hi⟩ := ih
      use .restrict f i
      grind [Witness.eval]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ K.toGrothendieck ≤ J

Tactic:
rw [toGrothendieck_le_iff_le_toPrecoverage]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ K ≤ J.toPrecoverage
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h✝ :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
X : Over S₀
b : X ⟶ Over.mk a
Y : Over S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h : ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows c
fac : Over.Hom.left b = Over.Hom.left d ≫ Over.Hom.left c
⊢ R.arrows (Over.Hom.left b)

Tactic:
simpa [fac] using R.downward_closed h d.left

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

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

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case fst
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (ConcreteCategory.hom
        (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op) ≫ biprod.fst))
      y =
    ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

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

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case snd
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (ConcreteCategory.hom
        (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op) ≫ biprod.snd))
      y =
    ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

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

Tactic:
· rw [Iso.addCommGroupIsoToAddEquiv_apply,
      Iso.addCommGroupIsoToAddEquiv_apply,
      ← AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply,
      Iso.hom_inv_id_apply, ← ConcreteCategory.comp_apply,
      biprod.lift_snd, Iso.inv_hom_id_apply]

Goal state after:
Module: Mathlib.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₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι π
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
⊢ Cofork.π (CokernelCofork.ofπ (πQ f₂ β) ⋯) ≫ 𝟙 Q = Cofork.π (CokernelCofork.ofπ (πQ f₂ β) ⋯) ≫ 0

Tactic:
by
      dsimp
      rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β]

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

Goal state before:
pp: case inl.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hd : d = b ∨ d ∈ s
hc : c ∈ s
⊢ b = c

Tactic:
obtain rfl | hd := hd

Goal state after:
case inl.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
c d : α
hc : c ∈ s
h : d * d = c * c
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ d = c

case inl.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c ∈ s
hd : d ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
⊢ b = c

Tactic:
obtain rfl | hd := hd

Goal state after:
case inr.inl.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = d

case inr.inl.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
⊢ b = c

Tactic:
obtain rfl | hd := hd

Goal state after:
case inr.inr.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c

case inr.inr.inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

Tactic:
abs_cast,

Goal state after:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ √(∑ x_1, ↑(x x_1) ^ 2) = √↑k
Module: Mathlib.Combinatorics.Additive.FreimanHom

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

Tactic:
· simpa using fun a h ↦ hf.mapsTo (htA h)

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

Goal state before:
pp: case inr.inr.ha
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n

pp: case hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d - 1

Tactic:
· rwa [one_le_cast]

Goal state after:
case hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d - 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ≠ 0

Tactic:
rwa [cast_ne_zero]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
⊢ ↑(#F) * ↑(#B) = ↑(#(F * B))

Tactic:
card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF,

Goal state after:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
⊢ ↑(#F) * ↑(#B) = ↑(#F * #B)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ √(log ↑N)

pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N

Tactic:
· apply log_two_mul_two_le_sqrt_log_eight.trans
      apply Real.sqrt_le_sqrt
      exact log_le_log (by simp) (mod_cast hN₃)

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (↑(nValue N))⁻¹ ≠ 0

Tactic:
exact (rpow_pos_of_pos hN₀ _).ne'

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:

Tactic:
_ ≤ (N ^ (nValue N : ℝ)⁻¹ / rexp 1 : ℝ) ^ (n - 2) / n := ?_
    _ < _ := by gcongr; exacts [(tsub_pos_of_lt hn₂).ne', bound hN]
    _ ≤ rothNumberNat ((2 * dValue N - 1) ^ n) := bound_aux hd.ne' hn₂.le
    _ ≤ rothNumberNat N := mod_cast rothNumberNat.mono this

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ (↑N ^ (↑(nValue N))⁻¹ / rexp 1) ^ (n - 2) / ↑n
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)

Tactic:
have : Nontrivial s := s.bot_or_nontrivial.resolve_left hs

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝¹ : Fact (1 < n)
this✝ : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
this : Nontrivial ↥s
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ SimpleGraph.comap (⇑f) (SimpleGraph.map (⇑f) G) = G

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ G.IsUniversal v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1

Tactic:
· rw [← G.insert_neighborFinset_eq_univ v, ← Finset.card_eq_iff_eq_univ]
    simp [h, Nat.sub_add_cancel <| Fintype.card_pos_iff.mpr ⟨v⟩]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
x : V
inst✝¹ : Fintype ↑(G.neighborSet x)
inst✝ : Fintype ↑(G'.neighborSet (f x))
⊢ G'.degree (f x) = G.degree x

Tactic:
by
  rw [← card_neighborSet_eq_degree, ← card_neighborSet_eq_degree,
    ← Fintype.card_congr (mapNeighborSet f x).symm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
P : Finpartition ⊥
⊢ P = default

Tactic:
ext a
      exact iff_of_false (fun h ↦ P.ne_bot h <| le_bot_iff.1 <| P.le h) (notMem_empty a)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
⊢ (image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset).sup id = s

Tactic:
refine (Finset.sup_le fun t ht ↦ ?_).antisymm fun a ha ↦ ?_
      · rw [mem_image] at ht
        obtain ⟨A, _, rfl⟩ := ht
        exact s.filter_subset _
      · rw [mem_sup]
        refine
          ⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t},
            mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
            mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩
        rw [mem_filter]
        exact and_iff_right ht

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
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) ≫
        (t.eTruncLT.obj b').map
            ((t.eTruncGE.obj a').map
              ((t.eTruncLT.map (φ.app 1)).app X ≫ (t.eTruncLTι ((mk₁ (homOfLE hab')).obj 1)).app X)) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)

Tactic:
simp [↓Functor.map_comp, t.eTruncLTGEIsoGELT_hom_app_fac]

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 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).2)

Tactic:
rw [nonuniformWitnesses, dif_pos h]
  exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1

Goal state after: