mathlib-initiative/mathlib-tactics huggingface dataset:
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) ↑(y₁, s₁).2 = (algebraMap R S) (y₁, s₁).1
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑(y₂, s₂).2 = (algebraMap R S) (y₂, s₂).1
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
dsimp only at e₁ e₂ ⊢

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 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: case refine_2
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 : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
· rintro ⟨x, -, hx⟩
    obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M x
    use algebraMap R S s
    rw [mul_comm, Subtype.coe_mk, e]
    refine Set.mem_image_of_mem (algebraMap R S) (mem_nonZeroDivisors_iff_right.mpr ?_)
    intro z hz
    apply IsLocalization.injective S hM
    rw [map_zero]
    apply hx
    rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
⊢ IsFractionRing S T

Tactic:
have := IsFractionRing.nontrivial R T
  have := (algebraMap S T).domain_nontrivial
  apply isFractionRing_of_isLocalization M S T
  intro x hx
  rw [mem_nonZeroDivisors_iff_ne_zero]
  intro hx'
  apply @zero_ne_one S
  rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]
  exact ⟨⟨x, hx⟩, by simp [hx']⟩

Goal state after:
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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal],
    Function.Injective
      ⇑((IsLocalizedModule.map P.primeCompl (Algebra.linearMap R (Rₚ P)) ↑(IsScalarTower.toAlgHom R S (Sₚ P)))
          (Algebra.linearMap R S))

Tactic:
intro p hp

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
        (Algebra.linearMap R S))
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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal],
    Function.Surjective
      ⇑((IsLocalizedModule.map P.primeCompl (Algebra.linearMap R (Rₚ P)) ↑(IsScalarTower.toAlgHom R S (Sₚ P)))
          (Algebra.linearMap R S))

Tactic:
intro p hp

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ Function.Surjective
    ⇑((IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
        (Algebra.linearMap R S))
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_1
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 τ
t : T
⊢ t ∈ τ → ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
ht

Goal state after:
case refine_1
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 τ
t : T
ht : t ∈ τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
I : Ideal R
⊢ Submodule.map (↑(TensorProduct.lid R M)) (map (Submodule.subtype I) LinearMap.id).range = I • ⊤

Tactic:
← LinearMap.range_comp,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
I : Ideal R
⊢ (↑(TensorProduct.lid R M) ∘ₗ map (Submodule.subtype I) LinearMap.id).range = I • ⊤
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 : 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
⊢ Function.Bijective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

Tactic:
constructor
  · suffices ∀ a ∈ s, ∀ b ∈ s, b ∉ P → ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P,
        x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b) by
      simpa [Function.Injective, (IsLocalization.mk'_surjective p.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq', Subtype.ext_iff, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, IsLocalization.eq_iff_exists p.primeCompl]
    intro a _ b _ _ c _ d _ _ x hxP e
    obtain ⟨t, ⟨htP, -⟩, ht⟩ := H.ge (Set.mem_univ x)
    exact ⟨_, ‹P.IsPrime›.mul_notMem htP hxP, ht, by simp [mul_assoc, e]⟩
  · suffices ∀ y, ∀ z ∉ P, ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y) by
      simpa [(IsLocalization.mk'_surjective p.primeCompl).exists,
        (IsLocalization.mk'_surjective P.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, Function.Surjective] using this
    intro y z hzP
    obtain ⟨a, ⟨haP, has⟩, ha⟩ := H.ge (Set.mem_univ y)
    obtain ⟨b, ⟨hbP, hbs⟩, hb⟩ := H.ge (Set.mem_univ z)
    exact ⟨_, mul_mem ha hbs, _, P.primeCompl.mul_mem (mul_mem hbP hzP) haP, mul_mem hb has, 1,
      P.primeCompl.one_mem, by ring⟩

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨α, hα : α ∉ p, e⟩ := s.prop

Goal state after:
case refine_2
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

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

Tactic:
refine Finset.prod_congr rfl ?_

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
⊢ motive f

Tactic:
rcases f.exists_T_pow with ⟨n, f', hf⟩
  rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub,
    ← mul_assoc, ← hf]
  exact mul_T ..

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

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

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

Tactic:
· simp only [a0, map_zero, zero_mul, degree_zero, bot_le]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ (C a * T n).degree ≤ ↑n
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

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

Tactic:
simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = diagonal (fun i ↦ ∏ j ∈ univ.erase i, v j) i j
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
⊢ (eval₂ f x) (C r) = f r

Tactic:
rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]

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

Goal state before:
pp: case pos
𝕜 : 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
hni : 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 : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]

Goal state after:
case pos
𝕜 : 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
hni : n = ↑i
this : ¬n.succ ≤ ↑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
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).det • (diagonal v).adjugate).diag * v) i = 1 i

Tactic:
diag_smul,

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.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
⊢ (v * (⅟(diagonal v).det • (diagonal v).adjugate).diag) i = 1 i

Tactic:
diag_smul,

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
⊢ (v * ⅟(diagonal v).det • (diagonal v).adjugate.diag) i = 1 i
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 α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
by
  obtain ⟨_⟩ := hA.nonempty_invertible
  obtain ⟨_⟩ := hC.nonempty_invertible
  obtain ⟨iAC⟩ := hAC.nonempty_invertible
  simp only [← invOf_eq_nonsing_inv] at iAC
  let := invertibleAddMulMul A U C V
  simp only [← invOf_eq_nonsing_inv]
  apply invOf_add_mul_mul

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

Goal state before:
pp: α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ b j ≤ k

Tactic:
exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ (matPolyEquiv m).coeff k i j = (m i j).coeff k

Tactic:
by
  refine Matrix.induction_on' m ?_ ?_ ?_
  · simp
  · intro p q hp hq
    simp [hp, hq]
  · intro i' j' x
    rw [matPolyEquiv_coeff_apply_aux_2]
    dsimp [single]
    split_ifs <;> rename_i h
    · constructor
    · simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = eval M (matPolyEquiv M.charmatrix.adjugate * (X - C M))
⊢ (aeval M) M.charpoly = 0

Tactic:
eval_mul_X_sub_C

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = 0
⊢ (aeval M) M.charpoly = 0
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)

Tactic:
by
  simp only [← nonempty_invertible_iff_isUnit,
    (invertibleEquivFromBlocks₁₁Invertible A B C D).nonempty_congr]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
exact isUnit_sub_one hnil

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsRight R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent x

Tactic:
rw [mul_pow h_comm] at hk

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsRight R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent x
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsLeft R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent y

Tactic:
rw [mul_pow h_comm] at hk

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsLeft R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent y
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ Represents b 1 1

Tactic:
delta Matrix.Represents PiToModule.fromMatrix
  rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_one]
  ext
  rfl

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
M : Matrix n n R
⊢ M.trace = -(∏ i, (X - C (M i i))).coeff (Fintype.card n - 1)

Tactic:
Fintype.card,

Goal state after:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
M : Matrix n n R
⊢ M.trace = -(∏ i, (X - C (M i i))).coeff (#univ - 1)