mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : P.LiesOver p
E : Type u_6
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
⊢ Q.LiesOver p

Tactic:
← show _ = P.map σ from comap_symm (RingEquivClass.toRingEquiv σ)

Goal state after:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : P.LiesOver p
E : Type u_6
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = comap (↑σ).symm P
⊢ Q.LiesOver p
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: case mk.mk
R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
a₁✝ : A ⧸ p
a : A
a₂✝ : A ⧸ p
b : A
hab :
  (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) a) =
    (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) b)
⊢ Quot.mk (⇑(quotientRel p)) a = Quot.mk (⇑(quotientRel p)) b

Tactic:
apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _)

Goal state after:
R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
a₁✝ : A ⧸ p
a : A
a₂✝ : A ⧸ p
b : A
hab :
  (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) a) =
    (algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) b)
⊢ (algebraMap A B) (a - b) ∈ P
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case ih
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
rintro (c : Set (Ideal R)) hc hc' J' hJ'

Goal state after:
case ih
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent A

Tactic:
conv_rhs => rw [← this]

Goal state after:
R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A))
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' : Submodule R M
I : Submodule R R
⊢ restrictScalars R (localized' S p f (I • M')) =
    restrictScalars R (localized' S p (Algebra.linearMap R S) I • localized' S p f M')

Tactic:
restrictScalars_localized'_smul,

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' : Submodule R M
I : Submodule R R
⊢ restrictScalars R (localized' S p f (I • M')) = I • restrictScalars R (localized' S p f M')
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f a r ∈ localized₀ p f Q

Tactic:
refine ⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r
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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a

Tactic:
obtain ⟨m, hm⟩ := IsLocalization.eq.mp (hi'.symm.trans hj')

Goal state after:
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 J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : ↑m * (↑mj * i) = ↑m * (↑mi * j)
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ (IsLocalizedModule.map M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap (IsScalarTower.toAlgHom R B Bₚ).toLinearMap)
      f.toLinearMap =
    ↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap

Tactic:
by
  ext x
  exact DFunLike.congr_fun (mapExtendScalars_eq_toLinearMap_mapₐ M Rₚ Aₚ Bₚ f) x

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
hJ : J.IsMaximal
⊢ localized₀ J.primeCompl (g J) G.ker = ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range

Tactic:
← LinearMap.ker_localizedMap_eq_localized₀_ker J.primeCompl (g J) (h J) G

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
hJ : J.IsMaximal
⊢ ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker = ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
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 • Submodule.Quotient.mk (m ⊗ₜ[R] n)

Tactic:
← Submodule.Quotient.mk_smul,

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)) = Submodule.Quotient.mk ((RingHom.id A) a • m ⊗ₜ[R] n)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case left
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
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R✝ S
r : R✝
inst✝ : IsLocalization.Away r S
f : S →+* T
hf : (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R✝ S))

Tactic:
exact hPc _ _ (hPl S r) hf

Goal state after:
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ˣ
p : R[X]
⊢ (IsLocalization.lift ⋯) ((algebraMap R[X] R[T;T⁻¹]) p) = Polynomial.eval₂ f (↑x) p

Tactic:
IsLocalization.lift_eq,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
⊢ (eval₂RingHom f ↑x) p = Polynomial.eval₂ f (↑x) p
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
⊢ adjugate 1 = 1

Tactic:
by
  ext
  simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]

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

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uM
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Module.rank T P = Module.rank R M

Tactic:
by
  simpa using lift_rank_eq_of_le_nonZeroDivisors S f hp hpT bc

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 α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible A

Tactic:
by
  rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]
  infer_instance

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s = g 0 * r
⊢ g i = 0

Tactic:
exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x✝¹ x✝ : m
h : b x✝ < b x✝¹
⊢ -M x✝¹ x✝ = 0

Tactic:
hM h,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x✝¹ x✝ : m
h : b x✝ < b x✝¹
⊢ -0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ M i j + N i j = 0

Tactic:
hM h,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ 0 + N i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ M i j - N i j = 0

Tactic:
hM h,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ 0 - N i j = 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).det = 1

Tactic:
exact mul_invOf_self _

Goal state after:
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' = b'

Tactic:
rw [p] at H
  exact add_right_cancel H

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun n R A ((toFunAlgHom n R A) M) = M

Tactic:
induction M with

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
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
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (D - C * ⅟A * B)

Tactic:
letI iABCD' :=
    submatrixEquivInvertible (fromBlocks A B C D) (Equiv.sumComm _ _) (Equiv.sumComm _ _)
  letI iDCBA := iABCD'.copy _ (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm
  exact invertibleOfFromBlocks₂₂Invertible D C B A

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

Goal state before:
pp: case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ s.encard

Tactic:
Set.encard,

Goal state after:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ ENat.card ↑s
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : id (⨅ s, ⨅ (_ : span R s = p), s.encard) = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ toENat (⨅ s, #↑↑s)

Tactic:
id_eq

Goal state after:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ toENat (⨅ s, #↑↑s)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(↑s).encard ≤ #↑↑s

Tactic:
Set.encard,

Goal state after:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(ENat.card ↑↑s) ≤ #↑↑s
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
s : Set M
⊢ ↑(toNat (span R s).spanRank) ≤ s.encard

Tactic:
Set.encard,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(toNat (span R s).spanRank) ≤ ENat.card ↑s
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: case inr.e_6
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ 0 = ↑0

Tactic:
Subalgebra.coe_zero

Goal state after:
case inr.e_6
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ 0 = 0
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 : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ s.encard = ↑p.spanFinrank

Tactic:
Set.encard,

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
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ ENat.card ↑s = ↑p.spanFinrank
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.generators.encard.toNat = p.spanRank

Tactic:
Set.encard,

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
⊢ ↑(ENat.card ↑p.generators).toNat = p.spanRank
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
heq : p.generators = ∅
⊢ p = ⊥

Tactic:
rw [← p.span_generators, heq, span_empty]

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
⊢ ⊤.spanRank = p.spanRank

Tactic:
simpa using (spanRank_map_eq_of_injective _ p.subtype_injective ⊤).symm

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

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h✝ : Nonempty n
⊢ M.trace = -M.charpoly.nextCoeff

Tactic:
nontriviality

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h✝ : Nonempty n
a✝ : Nontrivial R
⊢ M.trace = -M.charpoly.nextCoeff
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, h', mul_assoc]

Goal state after:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (algebraMap R S) ((algebraMap T R) r) * ((algebraMap R S) t * s) =
    ((algebraMap R S).comp φ.symm.toRingHom) r * ((algebraMap R S) t * s)