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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
⊢ ∀ i < ⊤, ∀ᶠ (a : α) in l, g a ∈ Ioi i

Tactic:
intro x hx

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x

Tactic:
filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le

Goal state after:
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

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:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
⊢ ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a

Tactic:
intro x hx

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ z < x, Ioc z x ⊆ a
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
p : 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
⊢ ∀ ⦃x : AddCircle p⦄, x ∈ {↑a}ᶜ → ↑((equivIco p a) x) ∈ Ioo a (a + p)

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
p : 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x✝ : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
x : AddCircle p
hx : x ∈ {↑a}ᶜ
⊢ ↑((equivIco p a) x) ∈ Ioo a (a + p)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
⊢ f = g

Tactic:
rw [← Set.eqOn_univ, ← coe_image_Ico_eq p a]

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
⊢ EqOn f g (QuotientAddGroup.mk '' Ico a (a + p))
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)
n : ℕ
h : 0 < ↑n
⊢ ↑(↑n * (p / ↑n)) = 0

Tactic:
mul_div_cancel₀ _ h.ne',

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ ↑p = 0
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) → n • u = 0

Tactic:
rw [← addOrderOf_dvd_iff_nsmul_eq_zero]
    rintro ⟨m, -, rfl⟩
    constructor; rw [mul_comm, eq_comm]
    exact gcd_mul_addOrderOf_div_eq p m h

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[instTopologicalSpaceQuot, inst✝] (Quot.lift ((Icc a (a + p)).domRestrict f) ⋯)

Tactic:
exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_domRestrict.mp hc)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ

Tactic:
refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ π ≫ γ = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
rw [moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff]
  tauto

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
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
⊢ ∀ (s : Cone I.multicospan) (j : WalkingMulticospan J), lift s ≫ K.π.app j = s.π.app j

Tactic:
rintro E (a | b)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
a : J.L
⊢ lift E ≫ K.π.app (WalkingMulticospan.left a) = E.π.app (WalkingMulticospan.left a)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ lift E ≫ K.π.app (WalkingMulticospan.right b) = E.π.app (WalkingMulticospan.right b)
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
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ HasLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))

Tactic:
exact inferInstanceAs <| HasEqualizer (F.map f) (F.map g)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
⊢ ∀ {c : Cone (F ⋙ R)} (hc : IsLimit c), Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
intro c h

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ g.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_363✝

Tactic:
by rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
⊢ ∀ {c : Cocone (F ⋙ R)} (hc : IsColimit c), Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
intro c h

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_246✝ _proof_451✝

Tactic:
by rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
x : R
⊢ (algebraMap R (S ⧸ map (algebraMap R S) p)) x =
    (algebraMap (R ⧸ p) (S ⧸ map (algebraMap R S) p)) ((algebraMap R (R ⧸ p)) x)

Tactic:
Quotient.algebraMap_eq,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
x : R
⊢ (algebraMap R (S ⧸ map (algebraMap R S) p)) x = (algebraMap (R ⧸ p) (S ⧸ map (algebraMap R S) p)) ((mk p) x)
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝¹⁰ : CommSemiring A
B : Type u_3
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ map (algebraMap A C) (under A P) ≤ under C (map (algebraMap B D) P)

Tactic:
apply le_comap_of_map_le

Goal state after:
A : Type u_2
inst✝¹⁰ : CommSemiring A
B : Type u_3
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ map (algebraMap C D) (map (algebraMap A C) (under A P)) ≤ map (algebraMap B D) P
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' : Submodule R M
⊢ map f M' ≤ localized₀ p f M'

Tactic:
rintro - ⟨x, hx, rfl⟩
  rw [mem_localized₀]
  exact ⟨x, hx, 1, IsLocalizedModule.mk'_one p f x⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes ≤ sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
intro x hx

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ sInf I.minimalPrimes
⊢ x ∈ sInf {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Tactic:
intro x hx

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I)
⊢ x ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
⊢ M ≤ nonZeroDivisors R

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ∈ nonZeroDivisors R
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
s x : S
hx : x ∈ adjoin R ↑σ
t : S
ht : t ∈ adjoin R ↑σ
ht' : ⟨t, ht⟩ ∈ Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)
h :
  s * (algebraMap (↥(adjoin R ↑σ)) S) ↑(⟨x, hx⟩, ⟨⟨t, ht⟩, ht'⟩).2 =
    (algebraMap (↥(adjoin R ↑σ)) S) (⟨x, hx⟩, ⟨⟨t, ht⟩, ht'⟩).1
⊢ ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
exact ⟨t, ht, ht', h ▸ hx⟩

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
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
⊢ False

Tactic:
obtain ⟨t, ht⟩ := IsLocalization.eq.1 hxyz

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
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : ↑t * (↑⟨1, ⋯⟩ * ((rx * ↑sy + ry * ↑sx) * rz)) = ↑t * (↑(sx * sy * sz) * 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
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ False

Tactic:
suffices (t : R) * (sx * sy * sz) ∈ P from
        not_or_intro (mt hp.mem_or_mem <| not_or_intro sx.2 sy.2) sz.2
          (hp.mem_or_mem <| (hp.mem_or_mem this).resolve_left t.2)

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
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : ↑t * ((rx * ↑sy + ry * ↑sx) * rz) = ↑t * (↑sx * ↑sy * ↑sz)
⊢ ↑t * (↑sx * ↑sy * ↑sz) ∈ P
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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h₁ : EssFiniteType R S
h₂ : EssFiniteType S T
⊢ EssFiniteType R T

Tactic:
rw [essFiniteType_iff] at h₁ h₂ ⊢

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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h₁ : ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
h₂ : ∃ σ, ∀ (s : T), ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ s * t ∈ adjoin S ↑σ
⊢ ∃ σ, ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case right
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
y z : S
hzP : z ∉ P
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)

Tactic:
obtain ⟨a, ⟨haP, has⟩, ha⟩ := H.ge (Set.mem_univ y)

Goal state after:
case right
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ ↑P.primeCompl
has : a ∈ ↑s.toSubmonoid
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
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
⊢ J ≠ ⊤

Tactic:
by
    rintro rfl
    exact Ideal.IsMaximal.ne_top ‹_› (by simp)

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

Goal state before:
pp: case mp.refine_1
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ x ∈ a, ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Tactic:
rintro x hx
      exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, map_one, one_smul]⟩

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
a : R''
b : R'
c : S
⊢ (tensorQuotientTensorEquiv R'' e) (a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (b ⊗ₜ[R] c)) =
    (Ideal.Quotient.mk (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})) ((a * (algebraMap R' R'') b) ⊗ₜ[R] c)

Tactic:
by
  simp [Algebra.tensorQuotientTensorEquiv, ← Ideal.Quotient.mk_algebraMap, ← map_mul]

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
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.EssFiniteType

Tactic:
change Algebra.EssFiniteType R S

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ Algebra.EssFiniteType R S