mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B)) ≫ F.map (G.map (adj.counit.app B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B) ≫ G.map (adj.counit.app B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯)

Tactic:
← F.map_comp,

Goal state after:
case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯ ≫ homOfLE ⋯)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯)

Tactic:
← F.map_comp,

Goal state after:
case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯ ≫ homOfLE ⋯)
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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.η.app c.pt ≫ (newCone D c).π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
newCone_π_app,

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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.η.app c.pt ≫ T.map (c.π.app j) ≫ (D.obj j).a = 𝟙 c.pt ≫ c.π.app j
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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ (newCone D c).π.app j = T.map (t.lift (newCone D c)) ≫ (newCone D c).π.app j

Tactic:
newCone_π_app,

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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ T.map (c.π.app j) ≫ (D.obj j).a = T.map (t.lift (newCone D c)) ≫ T.map (c.π.app j) ≫ (D.obj j).a
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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ T.map (c.π.app j) ≫ (D.obj j).a = T.map ((newCone D c).π.app j) ≫ (D.obj j).a

Tactic:
newCone_π_app,

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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ T.map (c.π.app j) ≫ (D.obj j).a = T.map (T.map (c.π.app j) ≫ (D.obj j).a) ≫ (D.obj j).a
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 : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ (newCone D c).π.app j = s.pt.a ≫ t.lift (T.forget.mapCone s) ≫ c.π.app j

Tactic:
newCone_π_app,

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 : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (c.π.app j) ≫ (D.obj j).a =
    s.pt.a ≫ t.lift (T.forget.mapCone s) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map (reflexion ≫ left) = 𝟙 (F.obj zero)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map (reflexion ≫ right) = 𝟙 (F.obj zero)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WalkingReflexivePair
⊢ Nonempty (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
cases X with

Goal state after:
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
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (G.map A.a) =
    F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A))

Tactic:
← F.map_comp,

Goal state after:
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
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)) ≫ G.map A.a) =
    F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WalkingReflexivePair
⊢ IsConnected (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
cases X with

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 ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ ∀ (X : Fin (n + 1 + 1)), (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app X = eqToHom ⋯

Tactic:
by rintro ⟨_ | _, hi⟩ <;> simp

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

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

Tactic:
rw [← cancel_epi e₀.hom, e₀.hom_inv_id_assoc, ← reassoc_of% h₃, e₁.hom_inv_id,
            Category.comp_id]

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

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
hp : p ≠ ⊤
⊢ Nontrivial (B ⧸ P)

Tactic:
Quotient.nontrivial_iff,

Goal state after:
A : Type u_3
B : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
hp : p ≠ ⊤
⊢ P ≠ ⊤
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
⊢ r ∈ (map N.mkQ ⊤).annihilator ↔ r ∈ N.colon Set.univ

Tactic:
annihilator_map_mkQ_eq_colon (N := N) (P := ⊤),

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
⊢ r ∈ N.colon ↑⊤ ↔ r ∈ N.colon Set.univ
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

Tactic:
rw [IsLocalizedModule.mk'_smul]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
hf : IsNilpotent (LinearMap.restrict f hq)
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
by
  obtain ⟨n, hn⟩ := hf
  use n
  ext ⟨x, hx⟩
  replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩
  simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢
  rw [Module.End.pow_restrict, LinearMap.restrict_apply] at hn ⊢
  ext
  exact (congr_arg Subtype.val hn :)

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

Goal state before:
pp: case neg.succ.succ.a
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 = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ (I ^ 2) ^ n.succ = ⊥

Tactic:
rw [← pow_mul, eq_bot_iff, ← hI, Nat.succ_eq_add_one]
      apply Ideal.pow_le_pow_right (by lia)

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

Goal state before:
pp: case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

pp: case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
· introv e h₁ h₂ h₃
    apply h₁
    apply h₂
    exact
      h₃.map
        ((DoubleQuot.quotQuotEquivQuotSup I J).trans
              (Ideal.quotEquivOfEq (sup_eq_right.mpr e))).symm.toRingHom

Goal state after:
case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : ↑m * (↑mj * i) = ↑m * (↑mi * j)
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a

Tactic:
rw [← mul_assoc, ← mul_assoc, mul_comm, ← mul_comm (j : R)] at hm

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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * (↑m * ↑mj) = j * (↑m * ↑mi)
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a
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
b : ↥I
s : ↥M
h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b
c : ↥M
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ a * ↑(c * s) ∈ I

Tactic:
rw [mul_comm, Submonoid.coe_mul, mul_assoc, hc]

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
b : ↥I
s : ↥M
h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b
c : ↥M
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ ↑c * ↑b ∈ I
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A ⊗[R] R[X]
hp : invFun R A ((toFunAlgHom R A) p) = p
hq : invFun R A ((toFunAlgHom R A) q) = q
⊢ invFun R A ((toFunAlgHom R A) (p + q)) = p + q

Tactic:
simp only [map_add, invFun_add, hp, hq]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
p✝ : Submonoid R
inst✝¹³ : IsLocalization p✝ S
M : Type u_3
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : IsScalarTower R S M
A : Type u_4
B : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Flat A B
p : Ideal A
inst✝⁴ : p.IsPrime
P : Ideal B
inst✝³ : P.IsPrime
inst✝² : P.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p P
⊢ Module.Flat (Localization.AtPrime p) (Localization.AtPrime P)

Tactic:
rw [Module.flat_iff_of_isLocalization (Localization.AtPrime p) p.primeCompl]
  exact Module.Flat.trans A B (Localization.AtPrime P)

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

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
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
⊢ (algebraMap R S) (x * z') = (algebraMap R S) (y * z')

Tactic:
rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]

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

Goal state before:
pp: case left
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
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
t : S
ht : t * x ∈ s
htP : t ∈ ↑P.primeCompl
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
exact ⟨_, ‹P.IsPrime›.mul_notMem htP hxP, ht, by simp [mul_assoc, e]⟩

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

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

Tactic:
refine ⟨⟨x, coeSubmodule_injective S h ?_⟩⟩

Goal state after:
case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = R ∙ (algebraMap R S) x
x_mem : (algebraMap R S) x ∈ coeSubmodule S I
⊢ coeSubmodule S I = coeSubmodule S (R ∙ x)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : IsLocalization M R'
S' : Type u
inst✝² : CommRing S'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this✝ : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this : IsScalarTower S (Localization (Submonoid.map f M)) S'
⊢ P (IsLocalization.map S' f hy)

Tactic:
have : IsLocalization (T.map (algebraMap S (Localization (M.map f)))) S' :=
    IsLocalization.isLocalization_of_submonoid_le _ _ (M.map f) T hle

Goal state after:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : IsLocalization M R'
S' : Type u
inst✝² : CommRing S'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this✝¹ : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this✝ : IsScalarTower S (Localization (Submonoid.map f M)) S'
this : IsLocalization (Submonoid.map (algebraMap S (Localization (Submonoid.map f M))) T) S'
⊢ P (IsLocalization.map S' f hy)
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✝ : 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 : ℕ
⊢ (R ⧸ p ^ n) ≃ₐ[R] Rₚ ⧸ maximalIdeal Rₚ ^ n

Tactic:
by
  refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_
  · simp_rw [ofId_apply, ← RingHom.mem_ker, ← SetLike.le_def]
    rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]
  · refine Ideal.Quotient.liftₐ _
      (IsLocalization.liftAlgHom (f := Ideal.Quotient.mkₐ R (p ^ n)) fun (u : p.primeCompl) ↦
        Ideal.Quotient.isUnit_mk_pow_of_notMem _ <| mem_primeCompl_iff.mp u.prop) fun x hx ↦ ?_
    obtain ⟨a, b, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
    rw [IsLocalization.mk'_mem_iff, ← Ideal.mem_under, under_maximalIdeal_pow p] at hx
    simpa [lift_mk', Quotient.eq_zero_iff_mem] using hx
  · rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
    exact IsLocalization.algHom_ext (W := p.primeCompl) (A := R) (by ext)
  · rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
    ext

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

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
⊢ ∃ α ∉ p, α • x ∈ pS

Tactic:
have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s : ↥(algebraMapSubmonoid S p.primeCompl)
hy : (algebraMap S Sₚ) x * (algebraMap S Sₚ) ↑(y, s).2 = (algebraMap S Sₚ) ↑(y, s).1
⊢ ∃ α ∉ p, α • x ∈ pS
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i, B (g i) i = (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff 0

Tactic:
coeff_zero_prod

Goal state after:
case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i, B (g i) i = ∏ i, ((X • A.map ⇑C + B.map ⇑C) (g i) i).coeff 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m - n) = T (m + -n)

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m + -n) = T (m + -n)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case e_b
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j : n
⊢ (∑ x ∈ s, fun j ↦ f j x) j = ∑ x ∈ s, f j x

Tactic:
apply Finset.sum_apply

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ (C a * T n).degree ≤ ↑n

Tactic:
exact (degree_C_mul_T n a a0).le

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ t.inv.toMatrix * t.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix = 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ t.toMatrix * t.inv.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix = 1