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

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n) a = f a ^ n
⊢ (f ^ (n + 1)) a = f a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n) a = f a ^ n
⊢ (f ^ n * f) a = f a ^ (n + 1)
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n) a = f a ^ n
⊢ (f ^ n * f) a = f a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n) a = f a ^ n
⊢ (f ^ n * f) a = f a ^ n * f a
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: case refine_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x ↦ (AddMonoidHom.mul x.1) x.2) (0, 0)

Tactic:
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (⇑(AddMonoidHom.mul x)) 0

Tactic:
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: case refine_3
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R), ContinuousAt (fun x ↦ (AddMonoidHom.mul x) y) 0

Tactic:
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Tactic:
have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset
  simpa using! this

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ 0 = |C * 0|

Tactic:
simp_rw [mul_zero, abs_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, |f b / a|ₘ < ε

Tactic:
by
  simp [nhds_eq_iInf_mabs_div, mabs_div_comm a]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ ((PartialEquiv.refl α).trans e).source = e.source

Tactic:
simp [trans_source, preimage_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)

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

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

Goal state after:
case hs
α : 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 η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝

Tactic:
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f a✝ < f y
h₂ : ¬f x✝ < f y
⊢ ∃ y_1, a✝ < y_1 ∧ f y_1 ≤ f y
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
ha : ∃ u, a < u
⊢ 𝓝[≥] a = ⨅ u, ⨅ (_ : a < u), 𝓟 (Ico a u)

Tactic:
simp only [nhdsGE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Iio_inter_Ici]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
⊢ { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
      { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T ↔
    S ≤ T

Tactic:
refine ⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩

Goal state after:
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
    { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T
⊢ S ≤ T
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
⊢ S.Exact ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
S.exact_iff_epi_toCycles,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi S.toCycles ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
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
z₂ : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
by simp [← cancel_mono S.iCycles, liftCycles_i]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case right
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ⋯
⊢ Function.Surjective ⇑(hom φ)

Tactic:
· intro x
        obtain ⟨a, ha⟩ := h₂ x.1.1 x.1.2 (by grind)
        cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w : ∀ (n : ToType N), (hom g) ((hom (cokernel.π f)) n) = (hom h) ((hom (cokernel.π f)) n)
x : CC N
⊢ (hom (coequalizer.π f 0 ≫ g)) x = (hom (coequalizer.π f 0 ≫ h)) x

Tactic:
simpa using w x

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

Goal state before:
pp: case refine_2
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
⊢ { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ } ≫ (beckCoalgebraFork X).ι = s.ι

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}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }

Tactic:
· ext
      simpa [← T.ε.naturality_assoc, T.left_counit_assoc] using! h₁ =≫ T.ε.app ((T : C ⥤ C).obj X.A)

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}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: 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
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
⊢ F.map hij ≫ app ⟨j, hj⟩ = app ⟨i, hi⟩ ≫ G.map hij

Tactic:
have hij' := leOfHom hij

Goal state after:
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
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
hij' : ⟨i, hi⟩ ≤ ⟨j, hj⟩
⊢ F.map hij ≫ app ⟨j, hj⟩ = app ⟨i, hi⟩ ≫ G.map hij
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: 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✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
      R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    X.a ≫ (reflectorAdjunction R).unit.app X.A

Tactic:
rw [← cancel_epi ((reflectorAdjunction R).unit.app X.A)]

Goal state after:
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✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫
      R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
        R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ ιPi I ≫ Pi.π I.left a = ι I a

Tactic:
by
  rw [ιPi, Category.assoc, ← Iso.eq_inv_comp, isoEqualizer]
  simp only [limit.isoLimitCone_inv_π,
    limit.cone_x, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app]
  rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π

Tactic:
dsimp [reflexiveCoforkEquivCofork]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
        (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).π =
    G.π
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t

Tactic:
rintro ⟨b, hb, h⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x ↦ a • x) b = 0
⊢ 0 ∈ t
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: 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
g h : ↥(MulAction.stabilizer G P)
a✝ : B ⧸ P
x : B
⊢ (algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B (g * h)) ⋯) (Quot.mk (⇑(quotientRel P)) x) =
    (algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B g) ⋯ *
        algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B h) ⋯)
      (Quot.mk (⇑(quotientRel P)) x)

Tactic:
exact congrArg (Ideal.Quotient.mk P) (mul_smul g h x)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x y : N
x✝¹ : x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
x✝ : y ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = x + y

Tactic:
rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ 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 : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

Tactic:
← show map_ideal M S I = Ideal.map (algebraMap R S) I by
    rw [map_ideal, Ideal.map, Ideal.span, Submodule.localized'_eq_span, Algebra.coe_linearMap],

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
z : S
⊢ z ∈ map_ideal M S I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.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
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
ha : a ∈ Ideal.under R (Ideal.map (algebraMap R S) I)
⊢ a ∈ I

Tactic:
rw [Ideal.mem_comap, IsLocalization.mem_map_algebraMap_iff M S] at ha

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
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
ha : ∃ x, (algebraMap R S) a * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1
⊢ a ∈ I
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
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m m' : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = (f P) m'
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']
  by_contra ne
  have ⟨P, mP, le⟩ := (eqIdeal R m m').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
  have ⟨s, hs⟩ := (IsLocalizedModule.eq_iff_exists P.primeCompl _).mp (h P)
  exact s.2 (le hs)

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

Goal state before:
pp: case mpr
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
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime

Tactic:
· refine fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩
    · rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ
    · intro x y hxy
      obtain ⟨a, s, ha⟩ := exists_mk'_eq M x
      obtain ⟨b, t, hb⟩ := exists_mk'_eq M y
      have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
      rw [mk'_mem_iff, ← Ideal.mem_comap] at this
      have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
      rw [Ideal.mem_comap, Ideal.mem_comap] at this₂
      rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]

Goal state after:
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
⊢ IsFractionRing S T

Tactic:
by
  have := IsFractionRing.nontrivial R T
  have := (algebraMap S T).domain_nontrivial
  apply isFractionRing_of_isLocalization M S T
  intro x hx
  rw [mem_nonZeroDivisors_iff_ne_zero]
  intro hx'
  apply @zero_ne_one S
  rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]
  exact ⟨⟨x, hx⟩, by simp [hx']⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ Ideal.map (algebraMap R R') (under R (Ideal.map (algebraMap S S') P)) = Ideal.map (algebraMap R R') p

Tactic:
← under_under (B := S),

Goal state after:
R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ Ideal.map (algebraMap R R') (under R (under S (Ideal.map (algebraMap S S') P))) = Ideal.map (algebraMap R R') p
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3.e_a
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y = (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y

pp: case mp.refine_3.e_a
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z' • y' = (mk' S 1 (z * z') * (algebraMap R S) ↑z) • y'

Tactic:
· rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]

Goal state after:
case mp.refine_3.e_a
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
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z' • y' = (mk' S 1 (z * z') * (algebraMap R S) ↑z) • y'
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
have H := coeff_eq_zero_of_natDegree_lt h

Goal state after:
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n) = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)