mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : pullback.lift x₂ x₃ h₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁

Tactic:
pullback.lift_snd_assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ { toFun := ⇑(hom (I.snd b')) } (↑x (J.snd b')) = (hom (I.fst b')) (↑x (J.fst b'))

Tactic:
exact (x.2 b').symm

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

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {W X Y Z : WalkingMulticospan J} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by
    rintro (_ | _) (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) (_ | _ | _) <;> rfl

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

Goal state before:
pp: J : MultispanShape
⊢ ∀ {W X Y Z : WalkingMultispan J} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by
    rintro (_ | _) (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) (_ | _ | _) <;> rfl

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero

Tactic:
apply Fan.IsLimit.hom_ext hc

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (i : J.L),
    (f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero) ≫ c.proj i =
      (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero ≫ c.proj i
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) =
      (match X with
        | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
        | WalkingMultispan.right a => π a) ≫
        ((Functor.const (WalkingMultispan J)).obj P).map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _) <;> dsimp

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.multispan.map (𝟙 (WalkingMultispan.left a✝)) ≫ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.snd a✝ ≫ π (J.snd a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.R
⊢ I.multispan.map (𝟙 (WalkingMultispan.right a✝)) ≫ π a✝ = π a✝ ≫ 𝟙 P
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.multispan.map (𝟙 (WalkingMultispan.left a✝)) ≫ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

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

Goal state before:
pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.fst a✝ ≫ π (J.fst a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

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

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.snd a✝ ≫ π (J.snd a✝) = (I.fst a✝ ≫ π (J.fst a✝)) ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

Goal state after:
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.L
⊢ I.snd a✝ ≫ π (J.snd a✝) = I.fst a✝ ≫ π (J.fst a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MultispanShape
I✝ : MultispanIndex J✝ C
K : Multicofork I✝
J : MultispanShape
I : MultispanIndex J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a✝ : J.R
⊢ I.multispan.map (𝟙 (WalkingMultispan.right a✝)) ≫ π a✝ = π a✝ ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

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

Goal state before:
pp: case refine_1
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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : C
B : adj.toComonad.Coalgebra
⊢ ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)

Tactic:
apply comparisonRightAdjointHomEquiv

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Submodule R M
hI : S.IsPrimary
⊢ (S.colon Set.univ).radical.IsPrime

Tactic:
refine isPrime_iff.mpr <| hI.imp (by simp) fun h x y ⟨n, hn⟩ ↦ ?_
  simp_rw [← mem_colon_iff_le, ← mem_radical_iff] at h
  refine or_iff_not_imp_left.mpr fun hx ↦ ⟨n, ?_⟩
  simp only [mul_pow, mem_colon, Set.mem_univ, true_imp_iff, mul_smul] at hn ⊢
  exact fun p ↦ (h (hn p)).resolve_right (mt mem_radical_of_pow_mem hx)

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

Goal state before:
pp: 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}
h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (fun x ↦ x ∈ S) m
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J

Tactic:
obtain ⟨p, hJp, hp⟩ := h

Goal state after:
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}
p : (Ideal R)ᵒᵈ
hJp : OrderDual.toDual J ≤ p
hp : Maximal (fun x ↦ x ∈ S) p
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ I.minimalPrimes ∧ p ≤ M
⊢ False

Tactic:
e

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ ∅ ∧ p ≤ M
⊢ False
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
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
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0 ⟨x, ⋯⟩
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢

Goal state after:
case h
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
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0
⊢ (LinearMap.restrict f hp ^ n) ⟨x, hx⟩ = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI : IsNilpotent I
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
⊢ P I

Tactic:
obtain ⟨n, hI : I ^ n = ⊥⟩ := hI

Goal state after:
S : Type u_1
inst✝ : CommRing S
I : Ideal S
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
n : ℕ
hI : I ^ n = ⊥
⊢ P I
Module: Mathlib.RingTheory.Localization.Ideal

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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ (algebraMap R S) x ∈ I

Tactic:
rw [← mk'_spec S x y, mul_comm]

Goal state after:
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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ (algebraMap R S) ↑y * mk' S x y ∈ 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
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
this : eqIdeal R x y = ⊤
⊢ x = y

Tactic:
by simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * ↑y
⊢ s ^ m * (x * s ^ n) ∈ I

Tactic:
e

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * ↑y
⊢ s ^ m * ↑y ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R'
⊢ (algebraMap R' S') x = (algebraMap R' S') y → ∃ c, ↑c * x = ↑c * y

Tactic:
e

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R'
e : (algebraMap R' S') x = (algebraMap R' S') y
⊢ ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid 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
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ x * (algebraMap R S) ↑s ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
e

Goal state after:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid 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
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ (algebraMap R S) (y, s).1 ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
⊢ (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
e

Goal state after:
case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ∃ c, ↑c * x = ↑c * y
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 ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
x

Goal state after:
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
⊢ x ∉ P → x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
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
⊢ x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
e

Goal state after:
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)
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Module: Mathlib.RingTheory.Localization.Submodule

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

Tactic:
rintro _ _ _ _ ⟨y, hy, z, rfl⟩ ⟨y', hy', z', rfl⟩

Goal state after:
case mp.refine_3
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
⊢ ∃ y_1 ∈ Submodule.span R a, ∃ z_1, mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 z_1 • y_1
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
c : B
⊢ ∀ (x : B ⧸ Ideal.map (algebraMap A B) I),
    ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        (c • x) =
      c •
        ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
          x

Tactic:
x

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
c : B
x : B ⧸ Ideal.map (algebraMap A B) I
⊢ ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
              (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
            Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
      (c • x) =
    c •
      ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        x
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ (x - y) * k = 0

Tactic:
rw [sub_mul, sub_eq_zero, h']

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ toLaurent (Polynomial.C r * f) = C r * toLaurent f

Tactic:
simp only [map_mul, Polynomial.toLaurent_C]

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

Goal state before:
pp: 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 : n
⊢ (∑ x ∈ s, A.cramer fun j ↦ f j x) i = A.cramer (fun j ↦ ∑ x ∈ s, f j x) i

Tactic:
rw [sum_cramer, cramer_apply]

Goal state after:
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 : n
⊢ (A.updateCol i (∑ x ∈ s, fun j ↦ f j x)).det = A.cramer (fun j ↦ ∑ x ∈ s, f j x) i
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible A

Tactic:
← conjTranspose_conjTranspose A,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible Aᴴᴴ
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
g : ℕ → R
⊢ ∀ (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0

Tactic:
x

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
g : ℕ → R
x : ℕ
⊢ ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (V * ⅟A * U * C * V)

Tactic:
simp_rw [Matrix.mul_assoc]

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

Tactic:
by
  have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
  rw [← List.take_length (l := listTransvecRow M), A]
  simpa using mul_listTransvecRow_last_col_take M i le_rfl

Goal state after: