mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ Submodule.Quotient.mk (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • S.mkQ (m ⊗ₜ[R] n)

Tactic:
Submodule.mkQ_apply,

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ Submodule.Quotient.mk (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • Submodule.Quotient.mk (m ⊗ₜ[R] n)
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ S

Tactic:
← Submodule.ker_mkQ S,

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ S.mkQ.ker
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ₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ ∃ a, (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) a = (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)

Tactic:
simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _),
      Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]

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ₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ ∃ a, (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) a) = (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)
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ₚ
n : ℕ
a : R
b : ↥p.primeCompl
hx : a ∈ p ^ n
⊢ (liftAlgHom ⋯) (mk' Rₚ a b) = 0

Tactic:
simpa [lift_mk', Quotient.eq_zero_iff_mem] using hx

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 : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ P f

Tactic:
by
  apply hP.ofIsLocalization hPi _ s hs
  intro r
  obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, hf⟩ := hT r
  exact ⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance,
    inferInstance, inferInstance, IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩

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

Goal state before:
pp: case h.refine_1
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
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [Algebra.smul_def]
      apply Ideal.mul_mem_right
      exact Ideal.mem_map_of_mem _ hγ

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

Goal state before:
pp: case e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
j x✝ : n
⊢ (b j • fun j_1 ↦ if j = j_1 then 1 else 0) x✝ = (b j • Pi.single j 1) x✝

Tactic:
simp [Pi.single_apply, eq_comm]

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

Goal state before:
pp: case refine_1
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
h : ⅟C * A = B
⊢ A = C * (⅟C * A)

Tactic:
Matrix.mul_invOf_cancel_left

Goal state after:
case refine_1
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
h : ⅟C * A = B
⊢ A = A
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ¬∀ (r : R) (s : ↥R⁰), ∃ r' s', ↑s' * r = r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
push Not at hS

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ∃ r s, ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : AddCommMonoid α
inst✝⁶ : AddCommMonoid β
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace

Tactic:
Matrix.trace,

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : AddCommMonoid α
inst✝⁶ : AddCommMonoid β
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ ∑ i, (((kroneckerMapBilinear f) A) B).diag i = (f (∑ i, A.diag i)) (∑ i, B.diag i)
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : AddCommMonoid α
inst✝⁶ : AddCommMonoid β
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ ∑ x ∈ Finset.univ ×ˢ Finset.univ, kroneckerMap (fun r s ↦ (f r) s) A B x x = ∑ x, ∑ x_1, (f (A x x)) (B x_1 x_1)

Tactic:
Finset.sum_product,

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : AddCommMonoid α
inst✝⁶ : AddCommMonoid β
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ ∑ x, ∑ y, kroneckerMap (fun r s ↦ (f r) s) A B (x, y) (x, y) = ∑ x, ∑ x_1, (f (A x x)) (B x_1 x_1)
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a ↦ ((mk R α β) a) 1).det ^ Fintype.card n * (B.map fun b ↦ ((mk R α β) 1) b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp -eta only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]

Goal state after:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a ↦ includeLeft a).det ^ Fintype.card n * (B.map fun b ↦ includeRight b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg.inr
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h✝ : Nonempty n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

Tactic:
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
      refine mt (fun hAB => ?_) hA
      rw [det_kronecker] at hAB
      exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)

Goal state after:
case neg.inr
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
⊢ toBlock 1 q p = 0

Tactic:
toBlock_one_disjoint

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
⊢ 0 = 0

α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
⊢ Disjoint q p
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).trace = N.trace

Tactic:
by rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R), (matPolyEquiv (single i j ((monomial n_1) a))).coeff k = single i j (((monomial n_1) a).coeff k)

Tactic:
· intro k x
    simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
    split_ifs <;>
      · funext
        simp

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
⊢ ∃ L L' D, M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod

Tactic:
rcases exists_list_transvec_mul_mul_list_transvec_eq_diagonal M with ⟨L, L', D, h⟩
  refine ⟨L.reverse.map TransvectionStruct.inv, L'.reverse.map TransvectionStruct.inv, D, ?_⟩
  suffices
    M =
      (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (L.map toMatrix).prod * M *
        ((L'.map toMatrix).prod * (L'.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod)
    by simpa [← h, Matrix.mul_assoc]
  rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]

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
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
⊢ x ^ i * y ^ j = 0

Tactic:
by_cases hi : m ≤ i

Goal state after:
case pos
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : m ≤ i
⊢ x ^ i * y ^ j = 0

case neg
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ x ^ i * y ^ j = 0
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
⊢ (↑I).FG

Tactic:
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.mul_inv ▸ one_le.mp le_rfl)

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ (↑I).FG
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ∃ s, s.card = p.spanFinrank ∧ span R ↑s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_encard_eq_spanFinrank h
  have s_f := Set.finite_of_encard_eq_coe hs₁
  refine ⟨s_f.toFinset, ⟨?_, by simpa using hs₂⟩⟩
  simpa [s_f.encard_eq_coe_toFinset_card, ENat.natCast_inj] using hs₁

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
⊢ lift.{v, u} p.spanRank ≤ a → ∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p

Tactic:
intro h
    obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
    exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ p.spanFinrank = 0 ↔ p = ⊥

Tactic:
refine ⟨fun heq ↦ ?_, fun h ↦ by simp [h]⟩

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
heq : p.spanFinrank = 0
⊢ p = ⊥
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M = ⊤.spanRank

Tactic:
have := nontrivial_of_invariantBasisNumber R
  obtain ⟨I, B⟩ := ‹Module.Free R M›
  rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B),
    Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _]

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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
⊢ a✝ ∈ Set.range ⇑f

Tactic:
obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc

Goal state after:
case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
n : ℕ
hn : a✝ = p.coeff n
⊢ a✝ ∈ Set.range ⇑f
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f (X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k) = p

Tactic:
Polynomial.map_add,

Goal state after:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f (X ^ p.natDegree) + map f (∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k) = p
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
calc
    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
x✝ : (p * q).natDegree < n ∨ n ≤ (p * q).natDegree
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
cases lt_or_ge (natDegree (p * q)) n with

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ x ∈ integralClosure R A

Tactic:
exact hx

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap A B) (mk' A ((algebraMap R B) x) h) = (algebraMap A B) ((algebraMap R A) x)

Tactic:
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ f ∈ vanishingIdeal (zeroLocus ↑I) ↔ f ∈ I.radical

Tactic:
rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]
    exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s = ⊤ ↔ s = ∅

Tactic:
by
  rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
⊢ I = ⊤

Tactic:
by_contra e

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
⊢ False
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
⊢ f.SurjectiveOnStalks ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩
  obtain ⟨y, r, c, hc, hr, e⟩ :=
    (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x
  simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr
  refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩
  apply hr.mul_right_injective
  apply hc.mul_right_injective
  simp only [← map_mul, ← mul_assoc, IsUnit.mul_val_inv, one_mul, e]

Goal state after: