mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b → x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)

Tactic:
rintro ⟨c, hc, rfl⟩
    simpa [update_le_update_iff]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ ∀ s_1 ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] s_1

Tactic:
rintro _ ⟨a, rfl | rfl⟩

Goal state after:
case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Ioi a)

case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : ↑x = ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
apply_fun equivIoc p a at h

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : (equivIoc p a) ↑x = (equivIoc p a) ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case H
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
p : 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.Tendsto (⇑(equivIco p a)) (𝓝 ↑z✝) (𝓝 ((equivIco p a) ↑z✝))

Tactic:
Filter.Tendsto,

Goal state after:
case H
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
p : 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (⇑(equivIco p a)) (𝓝 ↑z✝) ≤ 𝓝 ((equivIco p a) ↑z✝)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case H
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
p : 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.Tendsto (⇑(equivIoc p a)) (𝓝 ↑z✝) (𝓝 ((equivIoc p a) ↑z✝))

Tactic:
Filter.Tendsto,

Goal state after:
case H
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
p : 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (⇑(equivIoc p a)) (𝓝 ↑z✝) ≤ 𝓝 ((equivIoc p a) ↑z✝)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℕ
⊢ ↑(↑m / q * r) = m • ↑(r / q)

Tactic:
rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.one ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom = MonObj.one

Tactic:
exact ((IsZero.iff_id_eq_zero _).2 (Subsingleton.elim _ _)).eq_of_src _ _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
have h := (ShortComplex.mk _ _ c.condition).exact_of_g_is_cokernel
      (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by simp)))

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h : { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.Exact
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₂.X₁
hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
exact ⟨A₃, π₃ ≫ π₂ ≫ π₁, inferInstance, π₃ ≫ x₂, by simp only [assoc, hx₂, comp_zero],
      x₁, by simpa only [assoc] using hx₁⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ (sum ((f₁ + f₂) ≫ g) fun f' r ↦ r • F.map f') =
    ((f₁ + f₂).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

Tactic:
| add f₁ f₂ w₁ w₂ =>

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ (sum (single f' r ≫ (f₁ + f₂)) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'

Tactic:
| add f₁ f₂ w₁ w₂ =>

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : F.map f₁ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₁
w₂ : F.map f₂ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₂
⊢ F.map (f₁ + f₂) ≫ (α.app Y).hom = (α.app X).hom ≫ G.map (f₁ + f₂)

Tactic:
| add f₁ f₂ w₁ w₂ =>

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑f
x✝ : ↑f.shortComplexKer.X₂
⊢ (ConcreteCategory.hom f.shortComplexKer.g) x✝ = 0 ↔ x✝ ∈ Set.range ⇑(ConcreteCategory.hom f.shortComplexKer.f)

Tactic:
simp [shortComplexKer]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj P).map f ≫
        match Y with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
      (match X with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
        I.multicospan.map f

Tactic:
#adaptation_note /-- Proof repaired after leanprover/lean4#13363.
        The proof used to finish from this point as
        ```
        rintro (_ | _) (_ | _) (_ | _ | _) <;>
          dsimp <;> simp only [Category.id_comp, Category.comp_id]
        apply w
        ```
        The replacement proof is a short-term fix, and we request that the authors/maintainers of
        this file review the proof, and either approve it by removing this note,
        revise the proof or the prerequisites appropriately, or minimize a problem in lean4 that
        still needs addressing. -/
        rintro (_ | _) (_ | _) (_ | _ | _) <;>
          simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id] <;>
          dsimp <;> simp only [Category.id_comp]
        apply w

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (h.counit.app (L.obj (R.obj X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)

Tactic:
rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map left ≫
      match zero with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map left

pp: case right
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map right ≫
      match zero with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map right

pp: case reflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map reflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match zero with
      | zero => e₀
      | one => e₁) ≫
      G.map reflexion

pp: case leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map leftCompReflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map leftCompReflexion

pp: case rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map rightCompReflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map rightCompReflexion

pp: case id
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x✝ : WalkingReflexivePair
⊢ (F.map (Hom.id x✝) ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝ with
      | zero => e₀
      | one => e₁) ≫
      G.map (Hom.id x✝)

Tactic:
all_goals
      dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ F.map left ≫ e₀.hom ≫ e₀.inv = F.map left

Tactic:
e₀.hom_inv_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ F.map left ≫ 𝟙 (F.obj zero) = F.map left
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ F.map right ≫ e₀.hom ≫ e₀.inv = F.map right

Tactic:
e₀.hom_inv_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ F.map right ≫ 𝟙 (F.obj zero) = F.map right
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
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:
exact h i (by valid)

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
by_cases h : I + span {y} = ⊤

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical

case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical
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
⊢ localized₀ p f ⊥ = ⊥

Tactic:
← le_bot_iff

Goal state after:
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
⊢ localized₀ p f ⊥ ≤ ⊥
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
⊢ localized₀ p f (M' ⊓ M'') = localized₀ p f M' ⊓ localized₀ p f M''

Tactic:
by
  simp only [Submodule.ext_iff, Submodule.mem_inf, mem_localized₀]
  refine fun x ↦ ⟨by grind, ?_⟩
  rintro ⟨⟨i, hi, s, hs⟩, j, hj, t, ht⟩
  have h := ht.trans hs.symm
  rw [IsLocalizedModule.mk'_eq_mk'_iff] at h
  obtain ⟨k, hk⟩ := h
  refine ⟨(k * t) • i, ⟨M'.smul_of_tower_mem (k * t) hi, ?_⟩, k * s * t, ?_⟩
  · rw [mul_smul, hk, smul_smul]
    exact M''.smul_of_tower_mem (k * s) hj
  · rwa [mul_smul, hk, smul_smul, IsLocalizedModule.mk'_cancel_left]

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

Goal state before:
pp: case a.refine_1
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' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ ∀ r ∈ I, ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

Tactic:
intro r hr n hn

Goal state after:
case a.refine_1
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' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1 c, ↑c * ↑x_1.2 * x = ↑c * ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
← Submonoid.coe_mul

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1 c, ↑(c * x_1.2) * x = ↑c * ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
⊢ ∀ (y : ↥(Submonoid.map f M)), IsUnit ((algebraMap R' S') ↑y)

Tactic:
rintro ⟨_, y, hy, rfl⟩
    simpa only [← RingHom.comp_apply, H] using (IsLocalization.map_units S ⟨y, hy⟩).map g

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

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommSemiring S
R : Type u_4
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
⊢ FaithfulSMul R S

Tactic:
faithfulSMul_iff_algebraMap_injective,

Goal state after:
S : Type u_2
inst✝⁴ : CommSemiring S
R : Type u_4
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
⊢ Function.Injective ⇑(algebraMap R S)
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = R ∙ x
⊢ Submodule.IsPrincipal I

Tactic:
have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x
    obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem
    refine ⟨⟨x, coeSubmodule_injective S h ?_⟩⟩
    rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₁ b₂ : T
⊢ ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) ((a₁ * a₂) ⊗ₜ[R] (Ideal.Quotient.mk I) (b₁ * b₂)) =
    ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₁ ⊗ₜ[R] (Ideal.Quotient.mk I) b₁) *
      ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₂ ⊗ₜ[R] (Ideal.Quotient.mk I) b₂)

Tactic:
simp only [LinearEquiv.coe_coe, LinearEquiv.trans_apply, g,
      AlgebraTensorModule.tensorQuotientEquiv_apply_tmul, ← Ideal.Quotient.mk_eq_mk,
      ← Algebra.TensorProduct.tmul_mul_tmul]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₁ b₂ : T
⊢ (((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
        (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯)
      (Submodule.Quotient.mk (a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂)) =
    (((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
          (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯)
        (Submodule.Quotient.mk (a₁ ⊗ₜ[R] b₁)) *
      (((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
          (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯)
        (Submodule.Quotient.mk (a₂ ⊗ₜ[R] b₂))
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
f : S →ₐ[R] T
hf : Function.Surjective ⇑f
inst✝ : EssFiniteType R S
⊢ EssFiniteType R T

Tactic:
let := f.toAlgebra
  have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.Finite S T := .of_surjective (Algebra.linearMap S T) hf
  exact .comp R S T

Goal state after: