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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
rcases lt_trichotomy c 0 with (hc | rfl | hc)

Goal state after:
case inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

case inr.inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d

case inr.inr.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases (nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩

Goal state after:
case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
s : ↑S.X₃ → ↑S.X₂
hs : Function.RightInverse s ⇑(ConcreteCategory.hom S.g)
x₂ : ↑S.X₂
⊢ ∃ a,
    (fun x ↦
          match x with
          | (x₁, x₃) => (ConcreteCategory.hom S.f) x₁ + s x₃)
        a =
      x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])

Goal state after:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
s : ↑S.X₃ → ↑S.X₂
hs : Function.RightInverse s ⇑(ConcreteCategory.hom S.g)
x₂ : ↑S.X₂
x₁ : ↑S.X₁
hx₁ : (ConcreteCategory.hom S.f) x₁ = x₂ - s ((ConcreteCategory.hom S.g) x₂)
⊢ ∃ a,
    (fun x ↦
          match x with
          | (x₁, x₃) => (ConcreteCategory.hom S.f) x₁ + s x₃)
        a =
      x₂
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] A'
⊢ Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)

Tactic:
simp [← dual_rTensor_conj_homEquiv, dual_surjective_iff_injective]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : y = y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑y = ↑x'

Tactic:
hy,

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : y = y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑y' = ↑x'
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 : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ (equivIoc p a) ↑x = ⟨x, hx⟩

Tactic:
rw [← Equiv.eq_symm_apply, equivIoc, QuotientAddGroup.equivIocMod_symm_apply]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X X).hom ≫ MonObj.mul = MonObj.mul

Tactic:
by simp [add_comm]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom) (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk (((x, y), z).1.2, ((x, y), z).2))

Tactic:
μIso_hom_freeMk_tmul_freeMk

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) = freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2)
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
i : ℕ
S : ComposableArrows C (i + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ ⋯)).Exact
hi✝ : i + 2 ≤ i + 2
hi : i ≤ i
⊢ (S.sc ⋯ i hi✝).Exact

Tactic:
exact h'.exact 0

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ Epi (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
rw [epi_iff_surjective_up_to_refinements]
  constructor
  · intro h A y₂ hy₂
    obtain ⟨A₁, π₁, hπ₁, γ, hγ⟩ := h (S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ)
    obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ
    replace hγ := π₂ ≫= hγ
    simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements] at hγ
    obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ := hγ
    exact ⟨A₃, π₃ ≫ π₂ ≫ π₁, inferInstance, π₃ ≫ x₂, by simp only [assoc, hx₂, comp_zero],
      x₁, by simpa only [assoc] using hx₁⟩
  · intro h A γ
    obtain ⟨A₁, π₁, hπ₁, y₂, hy₂, fac⟩ := S₂.eq_liftCycles_homologyπ_up_to_refinements γ
    obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, y₁, hy₁⟩ := h y₂ hy₂
    refine ⟨A₂, π₂ ≫ π₁, inferInstance, S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ, ?_⟩
    simp only [assoc, fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements]
    exact ⟨A₂, 𝟙 _, inferInstance, y₁, by simpa only [id_comp] using hy₁⟩

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 : Discrete J),
    (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) j)) ((hom (piComparison F f)) x) =
      (hom (limit.π (Discrete.functor fun b ↦ F.obj (f b)) j)) ((hom (piComparison F f)) y)

Tactic:
intro ⟨j⟩

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 (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)
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ (s : Cone (pair M N)) (j : Discrete WalkingPair),
    ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right }))) ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j

Tactic:
rintro s (⟨⟩ | ⟨⟩) <;> rfl

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = s.ι.f ≫ T.ε.app X.A

Tactic:
← hm

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = (m ≫ (beckCoalgebraFork X).ι).f ≫ T.ε.app X.A
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
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (i.hom ≫ (adj.toMonad.transport i).μ) ≫ adj.unit = 𝟙 (L ⋙ R)

Tactic:
by
    rw [assoc, ← Iso.eq_inv_comp, comp_id, ← id_comp i.inv, Iso.eq_comp_inv, assoc,
      NatTrans.id_comm]
    ext X
    exact (adj.toMonad.transport i).right_unit X

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ T.map (c.ι.app j) ≫ lambda c t =
    T.map (T.map (c.ι.app j)) ≫ T.map (lambda c t) ≫ lambda c t

Tactic:
←
      Functor.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ T.map (c.ι.app j) ≫ lambda c t = T.map (T.map (c.ι.app j) ≫ lambda c t) ≫ lambda c t
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ (f a ⊓ s.inf f).IsPrimary

Tactic:
refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_

Goal state after:
case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ ((f a).colon Set.univ).radical = ((s.inf f).colon Set.univ).radical
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case ih.refine_1
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ b ∈ c, I ≤ b

Tactic:
exact fun _ hx => (hc hx).2

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

Goal state before:
pp: case neg.succ.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (0 + 1) = ⊥
⊢ P I

Tactic:
rw [pow_one] at hI
    exact (hI' hI).elim

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

Goal state before:
pp: 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⁻¹
⊢ (Ideal.Quotient.mk I) x * (Ideal.Quotient.mk I) y = 1

Tactic:
hy,

Goal state after:
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⁻¹
⊢ (Ideal.Quotient.mk I) x * ↑H.unit⁻¹ = 1
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
hx : x ∈ I
s : ↥M
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) x s * (algebraMap R S) ↑(⟨x, hx⟩, s).2 =
    (algebraMap R S) ↑(⟨x, hx⟩, s).1

Tactic:
by rw [← IsLocalization.mk'_eq_mk', IsLocalization.mk'_spec]

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

Goal state before:
pp: case mp.refine_2
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
J : Ideal S
h : J.IsPrime
⊢ ∀ {x y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J

Tactic:
· intro x y hxy
      rw [Ideal.mem_comap, map_mul] at hxy
      exact h.mem_or_mem hxy

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 y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False

Tactic:
have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalizedModule.eq_iff_exists (.powers r.1) _).mp (h r)

Goal state after:
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 y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
n : ℕ
eq : ⟨(fun x ↦ ↑r ^ x) n, ⋯⟩ • x = ⟨(fun x ↦ ↑r ^ x) n, ⋯⟩ • y
⊢ False
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 I' : { p // p.IsPrime }
⊢ { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I' ↔
    I ≤ I'

Tactic:
by
    constructor
    · exact fun h => show I.val ≤ I'.val from map_under M S I.val ▸
        map_under M S I'.val ▸ Ideal.map_mono h
    exact fun h x hx => h hx

Goal state after:
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ ht

Goal state after:
case refine_1
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ x ∈ τ, ∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

case refine_2
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ (r : S), ∃ s ∈ σ, IsUnit s ∧ s • (algebraMap S T) r ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

case refine_3
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ (x y : T),
    x ∈ adjoin S τ →
      y ∈ adjoin S τ →
        (∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
          (∃ s ∈ σ, IsUnit s ∧ s • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
            ∃ s ∈ σ, IsUnit s ∧ s • (x + y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

case refine_4
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ (x y : T),
    x ∈ adjoin S τ →
      y ∈ adjoin S τ →
        (∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
          (∃ s ∈ σ, IsUnit s ∧ s • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
            ∃ s ∈ σ, IsUnit s ∧ s • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_3
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ sy • sx • x + (algebraMap S T) sx * sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
Algebra.smul_def sy (sx • x)

Goal state after:
case refine_3
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sy * sx • x + (algebraMap S T) sx * sy • y ∈
    Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
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
⊢ x ∈ Submodule.span S a → ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Tactic:
intro h
    refine Submodule.span_induction ?_ ?_ ?_ ?_ h
    · rintro x hx
      exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, map_one, one_smul]⟩
    · exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, map_one, one_smul]⟩
    · rintro _ _ _ _ ⟨y, hy, z, rfl⟩ ⟨y', hy', z', rfl⟩
      refine
        ⟨(z' : R) • y + (z : R) • y',
          Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'), z * z', ?_⟩
      rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ←
        IsScalarTower.algebraMap_smul S (z' : R), smul_smul, smul_smul]
      congr 1
      · rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
      · rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]
    · rintro a _ _ ⟨y, hy, z, rfl⟩
      obtain ⟨y', z', rfl⟩ := exists_mk'_eq M a
      refine ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, ?_⟩
      rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul]

Goal state after: