mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case a
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ sSup (f ⁻¹' Iic z) ≠ a

Tactic:
· have : sSup (f '' f ⁻¹' Iic z) ≤ z := csSup_le (.image _ ne) fun _ ⟨b, hb, heq⟩ ↦ heq ▸ hb
          exact fun h ↦ this.not_gt ((h ▸ ha).trans_eq (hf.map_csSup ne bdd))

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m < n, ↑(↑m / ↑n * p) = u) → addOrderOf u ∣ n

Tactic:
rintro ⟨m, -, rfl⟩

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ addOrderOf ↑(↑m / ↑n * p) ∣ n
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one

pp: case refine_2.h₁.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
· simp

Goal state after:
case refine_2.h₁.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one

pp: case h₂.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
· simp

Goal state after:
case h₂.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0

Tactic:
by rw [← comp_τ₂, S.w₁₃, zero_τ₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) ((hom (piComparison F f)) x) =
    (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) { as := j })) ((hom (piComparison F f)) y)

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, piComparison_comp_π]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (F.map (Pi.π f j))) x = (hom (F.map (Pi.π f j))) y
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
x : PullbackObj r b
⊢ (hom r) (↑x).1 = (hom b) (↑x).2

Tactic:
by grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))

Tactic:
· simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ ((Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f) ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝

Tactic:
rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, fstPiMapOfIsLimit_proj]

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (Fan.mk X fun x ↦ (Iso.refl X).hom).proj (J.fst x✝) ≫ (ofParallelHoms J f g).fst x✝
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.succ.zero.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

pp: case zero.succ.zero.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
· simp

Goal state after:
case zero.succ.zero.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a✝ : J.R
⊢ (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
    (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
      ((Functor.const (WalkingMultispan J)).obj a.pt).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))

Tactic:
· simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ B ⟶ comparisonRightAdjointObj adj A

Tactic:
refine equalizer.lift (adj.homEquiv _ _ f.f) ?_

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ (adj.homEquiv B A.A) f.f ≫ G.map A.a = (adj.homEquiv B A.A) f.f ≫ adj.unit.app (G.1 A.A)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case h₀
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ app' (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) 0 ⋯ = app' (𝟙 F) 0 ⋯

pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ δ₀Functor.map (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) = δ₀Functor.map (𝟙 F)

Tactic:
· simp

Goal state after:
case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ δ₀Functor.map (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) = δ₀Functor.map (𝟙 F)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case h₀
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ app' (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) 0 ⋯ = app' (𝟙 G) 0 ⋯

pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ δ₀Functor.map (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) = δ₀Functor.map (𝟙 G)

Tactic:
· simp

Goal state after:
case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ δ₀Functor.map (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) = δ₀Functor.map (𝟙 G)
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], PreservesLimit (parallelPair f g) F

Tactic:
by intros; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this✝ : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], ReflectsLimit (parallelPair f g) F

Tactic:
by intros; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
hi : 0 < n + 1
⊢ mapSucc ⟨0, hi⟩ =
    ((fun i ↦
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨0, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' 0 (0 + 1) ⋯ hi ≫
        ((fun i ↦
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨0 + 1, ⋯⟩).hom

pp: case succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
i : ℕ
hi : i + 1 < n + 1
⊢ mapSucc ⟨i + 1, hi⟩ =
    ((fun i ↦
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨i + 1, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' (i + 1) (i + 1 + 1) ⋯ hi ≫
        ((fun i ↦
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨i + 1 + 1, ⋯⟩).hom

Tactic:
· simp

Goal state after:
case succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
i : ℕ
hi : i + 1 < n + 1
⊢ mapSucc ⟨i + 1, hi⟩ =
    ((fun i ↦
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨i + 1, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' (i + 1) (i + 1 + 1) ⋯ hi ≫
        ((fun i ↦
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨i + 1 + 1, ⋯⟩).hom
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ under A P = ⊥

Tactic:
hp,

Goal state after:
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ under A ⊥ = ⊥
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
⊢ S ⊓ T ≠ ⊤

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
⊢ (∃ m, (m ∈ M' ∧ m ∈ M'') ∧ ∃ s, IsLocalizedModule.mk' f m s = x) →
    (∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ s, IsLocalizedModule.mk' f m s = x

Tactic:
by grind

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
⊢ IsUnit x

Tactic:
have : Ideal.Quotient.mk I (x * y) = Ideal.Quotient.mk I 1 := by
      rw [map_one, map_mul, hy, IsUnit.mul_val_inv]

Goal state after:
case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
this : (Ideal.Quotient.mk I) (x * y) = (Ideal.Quotient.mk I) 1
⊢ IsUnit x
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : FiniteType R S
⊢ EssFiniteType R S

Tactic:
obtain ⟨s, hs⟩ := ‹FiniteType R S›

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : FiniteType R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ EssFiniteType R S
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : S
x : R
t : ↥M
e : s * (algebraMap R S) ↑(x, t).2 = (algebraMap R S) (x, t).1
⊢ ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Tactic:
exact ⟨_, IsLocalization.map_units S t, x, e.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : 0 = 1
⊢ False

Tactic:
rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
⊢ False
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
htz : ↑t = 0
⊢ False

Tactic:
exact t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ I = Ideal.comap (g.comp f) K

Tactic:
hIJ,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ Ideal.comap f J = Ideal.comap (g.comp f) K
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) I

Tactic:
hIJ,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) (Ideal.comap f J)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
J : Ideal S
inst✝ : (under R J).IsMaximal
m : Ideal S
maxm : m.IsMaximal
hm : under R J ≤ under R m
⊢ J.IsMaximal

Tactic:
rwa [← IsLocalization.map_under M S J, IsMaximal.eq_of_le ‹_› (IsPrime.under R m).ne_top hm,
    IsLocalization.map_under M S m]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ f.EssFiniteType

Tactic:
algebraize [f]
  change Algebra.EssFiniteType R S
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Field

Goal state before:
pp: x✝ : IsField ℤ
exists_pair_ne✝ : ∃ x y, x ≠ y
mul_comm✝ : ∀ (x y : ℤ), x * y = y * x
h : ∀ {a : ℤ}, a ≠ 0 → ∃ b, a * b = 1
this : 2 ≠ 0 → ∃ b, 2 * b = 1
⊢ False

Tactic:
by grind

Goal state after: