mathlib-initiative/mathlib-tactics huggingface dataset:
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 T : Submodule R M
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
⊢ (S ⊓ T).IsPrimary

Tactic:
obtain ⟨_, hT⟩ := hT

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
⊢ (S ⊓ T).IsPrimary
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ IsMinimalPrime p ↔ Minimal Ideal.IsPrime p

Tactic:
simp [Ideal.IsMinimalPrime]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ Nonempty ↑I.minimalPrimes

Tactic:
obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal I h

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
⊢ Nonempty ↑I.minimalPrimes
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), IsNilpotent (f x) → f x = 0

Tactic:
IsNilpotent,

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, f x ^ n = 0) → f x = 0
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:
smul_comm,

Goal state after:
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 : ↑x • IsLocalization.mk' S 1 x • (m - n) ∈ localized' S p f M'
⊢ Submodule.Quotient.mk m = Submodule.Quotient.mk n
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
⊢ Ideal.under R (Ideal.map (algebraMap R S) I) = I

Tactic:
have key : Disjoint (M : Set R) I.radical := by
    contrapose hM
    rw [Set.not_disjoint_iff] at hM ⊢
    obtain ⟨a, ha, k, hk⟩ := hM
    exact ⟨a ^ k, pow_mem ha k, hk⟩
  refine le_antisymm (fun a ha ↦ ?_) Ideal.le_comap_map
  rw [Ideal.mem_comap, IsLocalization.mem_map_algebraMap_iff M S] at ha
  obtain ⟨⟨b, s⟩, h⟩ := ha
  replace h : algebraMap R S (s * a) = algebraMap R S b := by
    simpa only [← map_mul, mul_comm] using h
  obtain ⟨c, hc⟩ := (IsLocalization.eq_iff_exists M S).1 h
  have : a * (c * s : M) ∈ I := by
    rw [mul_comm, Submonoid.coe_mul, mul_assoc, hc]
    exact I.mul_mem_left c b.2
  exact ((Ideal.isPrimary_iff.mp hI).2 this).resolve_right (Set.disjoint_left.mp key (c * s).2)

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

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
N : Submonoid S
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ ↑M
e : y * (algebraMap R S) z = (algebraMap R S) x
⊢ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Tactic:
exact ⟨⟨y, hy⟩, ⟨z, hz⟩, e.symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ = (algebraMap S T) x₂ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ = (algebraMap S T) x₂ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑s₁ * (algebraMap R T) ↑⟨↑s₂, ⋯⟩ =
      (algebraMap S T) x₂ * (algebraMap R T) ↑s₁ * (algebraMap R T) ↑⟨↑s₂, ⋯⟩ ↔
    (algebraMap S T) x₁ * (algebraMap R T) ↑s₁ = (algebraMap S T) x₂ * (algebraMap R T) ↑s₁
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
suffices algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) →
        ∃ a : N, algebraMap R S (a * (y₁ * s₂)) = algebraMap R S (a * (y₂ * s₁)) by
      have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
        (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
      have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
      simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂
      simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc,
        mul_right_comm _ (algebraMap R S s₂),
        (IsLocalization.map_units S s₁).mul_left_inj,
        (IsLocalization.map_units S s₂).mul_left_inj] at this
      rw [h₂, h₁] at this
      simpa only [mul_comm] using! this

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
⊢ (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_3
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ sx • sy • x + (algebraMap S T) sx * sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
smul_comm,

Goal state after:
case refine_3
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ sy • sx • x + (algebraMap S T) sx * sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case right
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
y : S
⊢ ∀ z ∉ P, ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)

Tactic:
z

Goal state after:
case right
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
y z : S
⊢ z ∉ P → ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
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'
this : IsLocalization (Submonoid.map (algebraMap S (Localization (Submonoid.map f M))) T) S'
heq :
  IsLocalization.map S' f hy =
    (algebraMap (Localization (Submonoid.map f M)) S').comp (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯)
⊢ P (IsLocalization.map S' f hy)

Tactic:
heq

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'
heq :
  IsLocalization.map S' f hy =
    (algebraMap (Localization (Submonoid.map f M)) S').comp (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯)
⊢ P
    ((algebraMap (Localization (Submonoid.map f M)) S').comp
      (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
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 : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P ((algebraMap R S).comp (id R))

Tactic:
apply hP.StableUnderCompositionWithLocalizationAwayTarget S r

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P (id R)
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 = A ^ k

Tactic:
h

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.Polynomial

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

Tactic:
h

Goal state after:
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • 1 + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (Fintype.card n) = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)
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:
by
  simp only [map_mul, Polynomial.toLaurent_C]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
⊢ ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0 → ∀ i ∈ commonDenomOfFinset M s • s, f i = 0

Tactic:
h

Goal state after:
R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
⊢ ∀ i ∈ commonDenomOfFinset M s • s, f i = 0
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
⊢ ∑ i ∈ s, f (commonDenomOfFinset M s • i) • id i = 0

Tactic:
have inj := (IsLocalization.smul_bijective A (commonDenomOfFinset M s)).injective

Goal state after:
R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
f : A → R
h : ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0
inj : Function.Injective fun s_1 ↦ commonDenomOfFinset M s • s_1
⊢ ∑ i ∈ s, f (commonDenomOfFinset M s • i) • id i = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
⊢ (fun x ↦ A * x) B = (fun x ↦ A * x) C → B = C

Tactic:
h

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : (fun x ↦ A * x) B = (fun x ↦ A * x) C
⊢ B = C
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.adjugate * (A * B) = A.adjugate * (A * C)

Tactic:
h

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.adjugate * (A * C) = A.adjugate * (A * C)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ B * A * A.adjugate = C * A * A.adjugate

Tactic:
h

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ C * A * A.adjugate = C * A * A.adjugate
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
⊢ (blockDiagonal fun i ↦ A <• ↑b) = blockDiagonal fun x ↦ b •> A

Tactic:
congr! 2
    ext
    simp [(Nat.cast_commute b _).eq]

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

Goal state before:
pp: case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'

Tactic:
have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
    mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)

Goal state after:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

Tactic:
h

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * B⁻¹ = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ((⅟(diagonal v)).diag * v) i = 1 i

Tactic:
invOf_eq,

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ((⅟(diagonal v).det • (diagonal v).adjugate).diag * v) i = 1 i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
⊢ (M * (List.take n (listTransvecRow M)).prod *
        transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
      (inr ()) (inl i) =
    if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
· have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using! hi
        · simpa only [hni.symm, not_le, or_false] using! Nat.lt_succ_iff_lt_or_eq.1 hi

Goal state after: