mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Ulift

Goal state before:
pp: J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))

Tactic:
classical
        rw [isColimit_iff_bijective_desc, ← Function.Bijective.of_comp_iff _
          (quotQuotUliftAddEquiv F).bijective, ← AddEquiv.coe_toAddMonoidHom,
          ← AddMonoidHom.coe_comp, Quot.desc_quotQuotUliftAddEquiv]
        exact ULift.up_bijective.comp ((isColimit_iff_bijective_desc c).mp (Nonempty.intro hc))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
⊢ ∀ (g : A ⟶ S₁.homology), g ≫ homologyMap φ = 0 → g = 0

Tactic:
γ

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
⊢ γ ≫ homologyMap φ = 0 → γ = 0
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
⊢ ∀ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ

Tactic:
γ

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ γ = x ≫ homologyMap φ
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
⊢ S.φ₂ ≫ S.L₂.g = 0

Tactic:
by simp only [φ₂, assoc, S.v₁₂.comm₂₃, pullback.condition_assoc, w₀₂_τ₃, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
· ext
    apply Comonad.right_counit

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Tactic:
rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ f.app ⟨i + 1, hi⟩ = g.app ⟨i + 1, hi⟩

Tactic:
· exact congr_app h₁ ⟨i, by valid⟩

Goal state after:
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
inst✝¹ : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cone (D ⋙ T.forget)
t : IsLimit c
A B : J
f : A ⟶ B
⊢ ((const J).obj (conePoint c t)).map f ≫ { f := c.π.app B, h := ⋯ } = { f := c.π.app A, h := ⋯ } ≫ D.map f

Tactic:
by
                ext1
                simpa using (c.w f).symm

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
r : R
⊢ r ∈ N.colon {x} ↔ r • x ∈ N

Tactic:
simp [mem_colon, forall_eq]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes → J ∈ {I.radical}

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
⊢ J ∈ {I.radical}
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
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False

Tactic:
obtain ⟨a, ha, t, e⟩ := h r

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : 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
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : mk' (f r) a t = (f r) m
⊢ False
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
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
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
mk'_eq_mul_mk'_one

Goal state after:
case neg
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
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn)) = (Ideal.Quotient.mk I) ((algebraMap R S) r * mk' S 1 ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : ∃ a ∈ Algebra.algebraMapSubmonoid S M, a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : CommSemiring Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)
⊢ (map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ)) (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap Rₚ Sₚ)

Tactic:
apply IsLocalizedModule.linearMap_ext p.primeCompl (Algebra.linearMap _ _)
    (IsScalarTower.toAlgHom R S Sₚ : S →ₗ[R] Sₚ)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : CommSemiring Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)
⊢ (map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ)) (Algebra.linearMap R S) ∘ₗ
      Algebra.linearMap R Rₚ =
    ↑R (Algebra.linearMap Rₚ Sₚ) ∘ₗ Algebra.linearMap R Rₚ
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
⊢ (Ideal.map (algebraMap R Rₚ) p).IsMaximal

Tactic:
by
  rw [map_eq_maximalIdeal]
  exact maximalIdeal.isMaximal Rₚ

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ (x + y) * (tx * ty) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]

Goal state after:
case h.add
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x * tx * ty + y * ty * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : 1 = y * x
⊢ y * x = 1

Tactic:
eq_comm

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y * x = 1
⊢ y * x = 1
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : 1 = y * x
⊢ y * x = 1

Tactic:
eq_comm

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : y * x = 1
⊢ y * x = 1
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ (∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) → Nonempty (OreSet S)

Tactic:
intro H

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
H : ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
⊢ Nonempty (OreSet S)
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ₚ
⊢ under S (Ideal.map (algebraMap S Sₚ) pS) = pS

Tactic:
eq_comm

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ₚ
⊢ pS = under S (Ideal.map (algebraMap S Sₚ) pS)
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
⊢ (A ^ k).IsSymm

Tactic:
IsSymm,

Goal state after:
α : Type u_1
n : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
⊢ (A ^ k)ᵀ = A ^ k
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ (A.map f).IsSymm

Tactic:
IsSymm,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ (A.map f)ᵀ = A.map f
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ (A.map f).IsSymm ↔ A.IsSymm

Tactic:
IsSymm,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ (A.map f)ᵀ = A.map f ↔ A.IsSymm
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ (A.map f)ᵀ = A.map f ↔ A.IsSymm

Tactic:
IsSymm,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ (A.map f)ᵀ = A.map f ↔ Aᵀ = A
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsSymm ↔ Aᵀ = A.map fun x ↦ xᵀ

Tactic:
IsSymm,

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A)ᵀ = (comp m m n n α) A ↔ Aᵀ = A.map fun x ↦ xᵀ
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ x ∈ Finset.univ, (sign x • ∏ i, (X • A.map ⇑C + B.map ⇑C) (x i) i).coeff (Fintype.card n) = sign x • ∏ i, A (x i) i

Tactic:
simp only [Finset.mem_univ, forall_true_left]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ n ∈ p.coeff.support, C (p.coeff n) * T n).coeff a

Tactic:
simp_rw [← single_eq_C_mul_T]

Goal state after:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ x ∈ p.coeff.support, AddMonoidAlgebra.single x (p.coeff x)).coeff a
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[T;T⁻¹]
⊢ r • f = C r * f

Tactic:
induction f using LaurentPolynomial.induction_on' with

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 α
hA : A.IsSymm
⊢ A.adjugate.IsSymm

Tactic:
IsSymm,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : A.IsSymm
⊢ A.adjugateᵀ = A.adjugate
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
⊢ (C r * f).smeval x = r • f.smeval x

Tactic:
induction f using LaurentPolynomial.induction_on' with

Goal state after:
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 α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ ⅟C * B = A ↔ A = ⅟C * B

Tactic:
eq_comm

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ A = ⅟C * B ↔ A = ⅟C * B
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 α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
⊢ B * ⅟C = A ↔ A = B * ⅟C

Tactic:
eq_comm

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
⊢ A = B * ⅟C ↔ A = B * ⅟C
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
have A :
      (listTransvecCol M)[n] =
        transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]

Goal state after:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
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
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N)

Tactic:
by
  ext ⟨i, i'⟩ ⟨j, j'⟩
  rfl

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 : Matrix n n α
inst✝¹ : Invertible A.det
inst✝ : Invertible A
⊢ ⅟A = ⅟A.det • A.adjugate

Tactic:
let := invertibleOfDetInvertible A
  convert! (rfl : ⅟A = _)

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 : Matrix n n α
inst✝ : StarRing α
⊢ (A.det⁻¹ʳ • A.adjugate)ᴴ = Aᴴ.det⁻¹ʳ • Aᴴ.adjugate

Tactic:
conjTranspose_smul,

Goal state after:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : StarRing α
⊢ star A.det⁻¹ʳ • A.adjugateᴴ = Aᴴ.det⁻¹ʳ • Aᴴ.adjugate
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
inst✝ : LinearOrder m
M : Matrix m m R
h : M.IsLowerTriangular
⊢ M.det = ∏ i, M i i

Tactic:
by
  rw [← det_transpose]
  exact det_of_isUpperTriangular h.transpose

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
    split_ifs <;> simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.map ⇑f).charpoly = Polynomial.map f M.charpoly

Tactic:
rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]

Goal state after: