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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (fun x_1 ↦ x * x_1) (𝓝[>] 0), p (x * ε)

Tactic:
exact h.comap fun ε => x * ε

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
a : α
b b' : β
hb' : b' ∈ {b}
⊢ const α b (const β a b') = b'

Tactic:
rw [eq_of_mem_singleton hb', const_apply]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ TendstoIxxClass Icc (𝓝 a) (𝓝 a)

Tactic:
by
  simp only [nhds_eq_order, iInf_subtype']
  refine
    ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_
  refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out <;> intro _ _
  exacts [ordConnected_Ioi, ordConnected_Iio]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Tactic:
ext ⟨x, y⟩ <;> simp; tauto

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)

Tactic:
← sub_mem_Ico_iff_left,

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x - toIcoDiv hp a x • p ∈ Ico a (a + p)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Tactic:
· intro h
    rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩
    rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩
    exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩

Goal state after:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact → S.Exact

Tactic:
· intro h
    refine Exact.mk hS (fun i hi => ?_)
    obtain rfl : i = 0 := by lia
    exact h

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.left.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).IsComplex

Tactic:
isComplex₂_iff

Goal state after:
case mp.left.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map' 0 1 isComplex₂_iff._proof_2
        isComplex₂_iff._proof_4 ≫
      (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map' 1 2
        isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).hom = (εIso R).hom ▷ (free R).obj X ≫ (μIso R (𝟙_ (Type u)) X).hom ≫ (free R).map (λ_ X).hom

Tactic:
rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id]

Goal state after:
R : Type u
inst✝ : CommRing R
X : Type u
⊢ 𝟙 ((free R).obj X) =
    (λ_ ((free R).obj X)).inv ≫ (εIso R).hom ▷ (free R).obj X ≫ (μIso R (𝟙_ (Type u)) X).hom ≫ (free R).map (λ_ X).hom
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex

Tactic:
isComplex₂_iff

Goal state after:
case mp.right.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4
        isComplex₂_iff._proof_5 =
    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
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
let x₂ := π₂ ≫ p ≫ pullback.fst _ _

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
left

Goal state after:
case none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ ∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y
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
b : J.R
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Tactic:
by
  rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk

Tactic:
by
  obtain rfl | rfl : i = j ∨ j = k := by lia
  · rw [map_id, id_comp]
  · rw [map_id, comp_id]

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ F.map' i (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + k + 1) ⋯ hj'

Tactic:
F.map'_comp i (i + k) (i + k + 1),

Goal state after:
case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ (F.map' i (i + k) ⋯ ⋯ ≫ F.map' (i + k) (i + k + 1) ⋯ hj') ≫ app ⟨i + k + 1, ⋯⟩ =
    app ⟨i, ⋯⟩ ≫ G.map' i (i + k + 1) ⋯ hj'
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ F.obj i = G.obj i

Tactic:
by fin_cases i <;> assumption

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
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A) ≅ X

Tactic:
refine Comonad.Coalgebra.isoMk ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ ((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).A ≅ X.A

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ ((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).a ≫
      (coreflectorAdjunction R).toComonad.map (Iso.hom ?refine_1) =
    Iso.hom ?refine_1 ≫ X.a
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
⊢ G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj ((𝟭 D).obj A.1))

Tactic:
rw [← G.map_comp, ← G.map_id]
    exact congr_arg G.map A.counit

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
⊢ ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i

Tactic:
intro ⟨i, hi⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i < n + 1 + 1
⊢ F.obj ⟨i, hi⟩ = G.obj ⟨i, hi⟩
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁶ : Q.LiesOver p
inst✝⁵ : P.LiesOver p
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
E : Type u_7
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
⊢ ∀ (r : A ⧸ p), (P.quotientEquiv Q (↑σ) h).toFun ((algebraMap (A ⧸ p) (B ⧸ P)) r) = (algebraMap (A ⧸ p) (C ⧸ Q)) r

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁶ : Q.LiesOver p
inst✝⁵ : P.LiesOver p
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
E : Type u_7
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
r✝ : A ⧸ p
x : A
⊢ (P.quotientEquiv Q (↑σ) h).toFun ((algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) x)) =
    (algebraMap (A ⧸ p) (C ⧸ Q)) (Quot.mk (⇑(quotientRel p)) x)
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ r • n ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')

Tactic:
rw [← algebraMap_smul S, Submodule.restrictScalars_mem]
    exact Submodule.smul_mem_smul ⟨_, hr, 1, by simp⟩ hn

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
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
⊢ localized₀ p f P ≤ localized₀ p f Q

Tactic:
by
  rintro - ⟨a, ha, r, rfl⟩
  refine ⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩
  simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
x : M
h : ∀ (r : ↑s), (f r) x = 0
⊢ ∀ (r : ↑s), (f r) x = (f r) 0

Tactic:
simpa only [map_zero] using h

Goal state after:
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
hp : I.IsPrime
hd : Disjoint ↑M ↑I
⊢ (Ideal.map (algebraMap R S) I).IsPrime

Tactic:
by
  rw [isPrime_iff_isPrime_disjoint M S, under_map_of_isPrime_disjoint M S hp hd]
  exact ⟨hp, hd⟩

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (((monomial n) 1).sum fun n r ↦ (monomial n) (a * (algebraMap R A) r)) = (monomial n) a

Tactic:
sum_monomial_index

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 1) = (monomial n) a

case refine_2.hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 0) = 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
by
    obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M z
    exact ⟨⟨y, _, h s.prop⟩, e⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
      ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
r : ↑s
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range

Tactic:
have := SetLike.ext_iff.mp <| H r

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
      ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
r : ↑s
this :
  ∀ (x : Nₚ r),
    x ∈ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker ↔
      x ∈ ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
⊢ Function.Surjective ⇑f

Tactic:
algebraize [f]
  let (r : s) : Algebra R (Sᵣ r) := (algebraMap S (Sᵣ r)).comp f |>.toAlgebra
  have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl
  have : ∀ r, IsLocalization.Away (algebraMap R S r.val) (Sᵣ r) := ‹_›
  let (r : s) : Algebra (Rᵣ r) (Sᵣ r) := localizationAlgebra (.powers r.val) S
  have (r : s) : IsScalarTower R (Rᵣ r) (Sᵣ r) :=
    .of_algebraMap_eq <| by simp [RingHom.algebraMap_toAlgebra]
  apply surjective_of_isLocalized_span s hs Rᵣ (fun r : s ↦ Algebra.linearMap _ _) _
    (fun r : s ↦ ((IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)) (Algebra.linearMap R S)
  simpa [IsLocalization.map_linearMap_eq_toLinearMap_mapₐ] using! h

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ y * x = 1

Tactic:
have := h _ (1 - y * x + x) _ eq <| by
    rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : x = 1 - y * x + x
⊢ y * x = 1
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_3
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✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
⊢ ((Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ maximalIdeal Rₚ ^ n)) ⋯).comp
          (Quotient.liftₐ (maximalIdeal Rₚ ^ n) (liftAlgHom ⋯) ⋯)).comp
      (Quotient.mkₐ R (maximalIdeal Rₚ ^ n)) =
    (AlgHom.id R (Rₚ ⧸ maximalIdeal Rₚ ^ n)).comp (Quotient.mkₐ R (maximalIdeal Rₚ ^ n))

Tactic:
exact IsLocalization.algHom_ext (W := p.primeCompl) (A := R) (by ext)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p)) ≤ I

Tactic:
intro x hx
  refine Ideal.mem_of_localization_maximal fun m hm ↦ ?_
  simp only [Submodule.mem_iInf, RingHom.mem_ker] at hx
  by_cases hle : I ≤ m
  · simp [hx _ _ hle]
  · simp [IsLocalization.AtPrime.map_eq_top_of_not_le _ hle]

Goal state after: