mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ single (f ≫ g) 1 = single (f ≫ g) (1 * 1)

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ single (f ≫ g) 1 = single (f ≫ g) 1
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
⊢ pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, φ₂, pullback.lift_fst_assoc,
    S.v₁₂.comm₁₂]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))

Tactic:
rw [← AddCommGrpCat.mono_iff_injective]
  constructor
  · intro
    infer_instance
  · apply Functor.mono_of_mono_map

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

Goal state before:
pp: case neg
J : MultispanShape
a b : J.L
h : ¬a = b
⊢ Subsingleton (left a ⟶ left b)

Tactic:
have : IsEmpty (left a ⟶ left b) := ⟨by rintro ⟨⟩; simp at h⟩

Goal state after:
case neg
J : MultispanShape
a b : J.L
h : ¬a = b
this : IsEmpty (left a ⟶ left b)
⊢ Subsingleton (left a ⟶ left b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.app (WalkingMulticospan.right b)

Tactic:
rw [app_right_eq_ι_comp_fst, reassoc_of% h]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a))) ≫ desc S =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst a))

Tactic:
Category.assoc

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst 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 (T.map (c.π.app j) ≫ (D.obj j).a) ≫ (D.obj j).a

Tactic:
← T.μ.naturality_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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.μ.app (D.obj j).A ≫ (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
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    (T.map (T.map (c.π.app j)) ≫ T.map (D.obj j).a) ≫ (D.obj j).a

Tactic:
Category.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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (c.π.app j)) ≫ T.map (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
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
⊢ lambda c t ≫ T.δ.app c.pt = lambda c t ≫ T.map (lambda c t)

Tactic:
by
    refine (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_
    rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc,
      ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _, assoc, ← Functor.map_comp, commuting,
      Functor.map_comp, ← assoc, commuting]
    simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc]
    rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

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

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

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

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

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ s⁻¹ • ((s * g * s⁻¹) • x - x) ∈ s⁻¹ • P

Tactic:
smul_sub,

Goal state after:
M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ s⁻¹ • (s * g * s⁻¹) • x - s⁻¹ • x ∈ s⁻¹ • P
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁸ : CommSemiring A
B : Type u_3
inst✝⁷ : CommSemiring B
C : Type u_4
inst✝⁶ : Semiring C
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst✝¹ : 𝔓.LiesOver P
inst✝ : P.LiesOver p
⊢ p = under A 𝔓

Tactic:
rw [P.over_def p, 𝔓.over_def P, under_under]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ ↑M'
⊢ ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = f x

Tactic:
exact ⟨x, hx, 1, IsLocalizedModule.mk'_one p f x⟩

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ ∀ (x : R), (∃ n, f (x ^ n) = 0) → f x = 0

Tactic:
← RingHom.mem_ker

Goal state after:
R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ ∀ (x : R), (∃ n, x ^ n ∈ ker f) → x ∈ ker f
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | I.IsMinimalPrime p}

Tactic:
refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩
    simp only [and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4

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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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 : ↥p
m n : N
e : IsLocalization.mk' S 1 x • ↑x • (m - n) ∈ localized' S p f M'
⊢ Submodule.Quotient.mk m = Submodule.Quotient.mk n

Tactic:
rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e

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

Goal state before:
pp: case mpr.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 : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : (algebraMap R S) (a * b) ∈ J
⊢ x ∈ J ∨ y ∈ J

Tactic:
← Ideal.mem_comap

Goal state after:
case mpr.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 : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J
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 : Ideal.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)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
⊢ m ∈ N

Tactic:
by
  let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)
  suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
  by_contra! ne
  have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  obtain ⟨a, ha, t, e⟩ := h r
  rw [← IsLocalizedModule.mk'_one (.powers r.1), IsLocalizedModule.mk'_eq_mk'_iff] at e
  have ⟨u, hu⟩ := e
  simp_rw [smul_smul] at hu
  exact Set.disjoint_right.mp disj (u * t).2 (by apply hu ▸ smul_mem _ _ ha)

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 A (Localization.AtPrime P)

Tactic:
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
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ p.primeCompl

Tactic:
intro x hx hx'

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R 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
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ ↑p
⊢ False
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' = (1 * mk' S 1 z') • y'

Tactic:
one_mul

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' • y'
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
⊢ (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))

Tactic:
by
    ext; simp [ψ, φ]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hT✝ : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)
r : ↑s
T : Type u
w✝² : CommRing T
w✝¹ : Algebra S T
w✝ : IsLocalization.Away (↑r) T
hT : P ((algebraMap S T).comp f)
⊢ P ((algebraMap S (Localization.Away ↑r)).comp f)

Tactic:
convert! hP'.1 _ (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hT✝ : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)
r : ↑s
T : Type u
w✝² : CommRing T
w✝¹ : Algebra S T
w✝ : IsLocalization.Away (↑r) T
hT : P ((algebraMap S T).comp f)
⊢ (algebraMap S (Localization.Away ↑r)).comp f =
    (Localization.algEquiv (Submonoid.powers ↑r) T).symm.toRingEquiv.toRingHom.comp ((algebraMap S T).comp f)
Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
⊢ False

Tactic:
have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))

Goal state after:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : ((MvPolynomial.eval fun p ↦ 1 p.1 p.2).mapMatrix (mvPolynomialX m m R)).det = det 1
⊢ False
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ (T n).degree = (1 * T n).degree

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ (T n).degree = (T n).degree
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ 1 * T (-↑n) = T (-↑n)

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ T (-↑n) = T (-↑n)
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
L : List (TransvectionStruct n R)
⊢ IsUnit (List.map (toMatrix ∘ TransvectionStruct.inv) L).prod

Tactic:
by
  refine IsUnit.of_mul_eq_one (L.reverse.map toMatrix).prod ?_
  rw [← reverse_inv_prod_mul_prod L.reverse, L.reverse_reverse]

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

Goal state before:
pp: case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i : n
⊢ 1 * ∏ x ∈ univ.erase i, v x = ∏ j ∈ univ.erase i, v j

Tactic:
one_mul

Goal state after:
case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i : n
⊢ ∏ x ∈ univ.erase i, v x = ∏ j ∈ univ.erase i, v j
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v).adjugate = diagonal fun i ↦ ∏ j ∈ univ.erase i, v j

Tactic:
by
  ext i j
  simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]
  obtain rfl | hij := eq_or_ne i j
  · rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
  · rw [diagonal_apply_ne _ hij]
    refine det_eq_zero_of_row_eq_zero j fun k => ?_
    obtain rfl | hjk := eq_or_ne k j
    · rw [updateCol_self, Pi.single_eq_of_ne' hij]
    · rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]

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

Goal state before:
pp: m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (1 * N).trace = N.trace

Tactic:
one_mul

Goal state after:
m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ N.trace = N.trace
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i ↦ B.map fun b ↦ f (a i) b)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]

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

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
x✝¹ x✝ : Matrix n m α
h : (fun x ↦ A * x) x✝¹ = (fun x ↦ A * x) x✝
⊢ x✝¹ = x✝

Tactic:
simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ * ·) h

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ B = C

Tactic:
by
  rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]

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

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ (fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
        (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j)).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

Tactic:
convert!
    det_fromBlocks_zero₂₁ (toBlock M p p) (toBlock M p fun j => ¬p j)
      (toBlock M (fun j => ¬p j) fun j => ¬p j)

Goal state after:
case e'_2
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ M.toBlock (fun j ↦ ¬p j) p = 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal

Tactic:
constructor
  · ext i j
    have : j = unit := by simp only
    simp [toBlocks₁₂, this, listTransvecCol_mul_mul_listTransvecRow_last_row M hM]
  · ext i j
    have : i = unit := by simp only
    simp [toBlocks₂₁, this, listTransvecCol_mul_mul_listTransvecRow_last_col M hM]

Goal state after: