mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ ∀ (X' X : C) (Y : adj.toComonad.Coalgebra) (f : X' ⟶ X) (g : (comparison adj).obj X ⟶ Y),
    (comparisonRightAdjointHomEquiv adj Y X') ((comparison adj).map f ≫ g) =
      f ≫ (comparisonRightAdjointHomEquiv adj Y X) g

Tactic:
intro A

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : C
⊢ ∀ (X : C) (Y : adj.toComonad.Coalgebra) (f : A ⟶ X) (g : (comparison adj).obj X ⟶ Y),
    (comparisonRightAdjointHomEquiv adj Y A) ((comparison adj).map f ≫ g) =
      f ≫ (comparisonRightAdjointHomEquiv adj Y X) g
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
⊢ PreservesColimit ((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) (monadicLeftAdjoint R ⋙ R)

Tactic:
exact preservesColimit_of_iso_diagram _ i.symm

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Flat R M
this : Flat (ULift.{t, u} R) R
⊢ Flat (ULift.{t, u} R) M

Tactic:
let _ := ULift.algebra'

Goal state after:
R : Type u
M : Type w
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Flat R M
this : Flat (ULift.{t, u} R) R
x✝ : (R : Type ?u.45) →
  (A : Type ?u.44) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra (ULift.{?u.46, ?u.45} R) A :=
  ULift.algebra'
⊢ Flat (ULift.{t, u} R) M
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ e₁.hom ≫ G.map right ≫ e₀.inv = F.map right

Tactic:
← reassoc_of% h₂,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ F.map right ≫ e₀.hom ≫ e₀.inv = F.map right
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ Function.Surjective ⇑(MulSemiringAction.toRingHom M R a)

Tactic:
by exact ha

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
R : Type u_4
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ Function.Surjective ⇑(MulSemiringAction.toRingHom M R a)

Tactic:
by exact ha

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

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ span R S
a✝ : r • x✝ ∈ N
⊢ r • a✝¹ • x✝ ∈ N

Tactic:
simp_all [smul_mem, smul_comm r]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.radical.IsMinimalPrime p} → p ∈ {p | I.IsMinimalPrime p}

Tactic:
rintro ⟨⟨a, ha⟩, b⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | I.IsMinimalPrime p}
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.IsMinimalPrime p} → p ∈ {p | I.radical.IsMinimalPrime p}

Tactic:
rintro ⟨⟨a, ha⟩, b⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | I.radical.IsMinimalPrime p}
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}

Tactic:
simp_rw [and_iff_right bot_le]

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ⊔ J ≤ q
⊢ p ≤ q

Tactic:
rw [sup_le_iff] at hq

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ≤ q ∧ J ≤ q
⊢ p ≤ q
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
x : ↥p
⊢ IsUnit ((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

Tactic:
Module.End.isUnit_iff

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
x : ↥p
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑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 R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))

Tactic:
IsLocalization.eq_iff_exists N T,

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₂
⊢ (∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr.map_units
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (y : ↥(Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S))),
    IsUnit ((algebraMap (↥(adjoin R ↑σ)) S) ↑y)

Tactic:
exact fun y ↦ y.prop

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
J : Ideal (Localization.AtPrime I)
h : Ideal.under R J = I
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime I) ≤ J

Tactic:
by
    simpa [← AtPrime.map_eq_maximalIdeal, ← h] using Ideal.map_comap_le

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

Goal state before:
pp: 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
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) x) = (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x)

Tactic:
Ideal.Quotient.mk_algebraMap,

Goal state after:
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
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) x = (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case 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ₚ
n : ℕ
⊢ p ^ n ≤ under R (maximalIdeal Rₚ ^ n)

Tactic:
under_maximalIdeal_pow p

Goal state after:
case 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ₚ
n : ℕ
⊢ p ^ n ≤ p ^ n
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 ∈ under R (maximalIdeal Rₚ ^ n)
⊢ (liftAlgHom ⋯) (mk' Rₚ a b) = 0

Tactic:
under_maximalIdeal_pow p

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ₚ
n : ℕ
a : R
b : ↥p.primeCompl
hx : a ∈ p ^ n
⊢ (liftAlgHom ⋯) (mk' Rₚ a b) = 0
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = 1
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree

Tactic:
rw [sg, one_smul]

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

Goal state before:
pp: case inr
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Module.rank S N = Module.rank R N

Tactic:
have inj := IsLocalization.injective S hp

Goal state after:
case inr
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank S N = Module.rank R N
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
s : Set N
hs : LinearIndepOn S id s
⊢ #↑↑⟨s, hs⟩ ≤ Module.rank R N

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R S).mpr inj

Goal state after:
case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
s : Set N
hs : LinearIndepOn S id s
this : FaithfulSMul R S
⊢ #↑↑⟨s, hs⟩ ≤ Module.rank R N
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
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
⊢ finrank R S = finrank R A

Tactic:
classical
  apply Cardinal.toNat_eq_of_forall_le_iff
  intro n
  simp_rw [Module.le_rank_iff_exists_finset, LinearIndepOn]
  constructor
  · rintro ⟨s, rfl, hs⟩
    let f : S ↪ A := ⟨algebraMap S A, FaithfulSMul.algebraMap_injective S A⟩
    exact ⟨s.map f, s.card_map f,
      (linearIndependent_equiv (s.equivMap f)).mp (LinearIndependent.algebraMap_comp_iff.mpr hs)⟩
  · rintro ⟨s, rfl, hs⟩
    exact ⟨finsetIntegerMultiple S⁰ s, card_finsetIntegerMultiple S⁰ s,
      linearIndepOn_finsetIntegerMultiple S⁰ hs⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (toLaurent f).coeff.support = Finset.map Nat.castEmbedding f.support

Tactic:
by simp [Polynomial.support]

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

Goal state before:
pp: case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
h✝ : Subsingleton R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
have := (algebraMap R T).codomain_trivial

Goal state after:
case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this✝ : NoZeroDivisors R
h✝ : Subsingleton R
this : Subsingleton T
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
r : R
⊢ r • ↑(x ^ 0) = r • 1

Tactic:
zpow_zero,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
r : R
⊢ r • ↑1 = r • 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
x : Sˣ
⊢ ↑(x ^ 0) = 1

Tactic:
zpow_zero,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
x : Sˣ
⊢ ↑1 = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0

Tactic:
blockDiagonal'_eq_blockDiagonal,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal' d ⟨i', i⟩ ⟨j', j⟩ = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly

Tactic:
have hMN :
      M * N = fromBlocks (-scalar m X + (A * B).map C) (-(X : R[X]) • A.map C) 0 (-scalar n X) := by
    simp [M, N, fromBlocks_multiply, smul_eq_mul_diagonal, -diagonal_neg]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case hmul
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := ⋯
⊢ ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A * B)

Tactic:
intro A

Goal state after:
case hmul
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun N ↦ N.det ≠ 0 ∧ P N
A : Matrix n n 𝕜
⊢ ∀ (B : Matrix n n 𝕜), Q A → Q B → Q (A * B)
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a = b
H : a' + b ≤ b' + a
⊢ a' ≤ b'

Tactic:
by
  rwa [p, add_le_add_iff_right] at H

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · rwa [Commute.isNilpotent_mul_left_iff (commute_X P) (by simp)] at h
  · rintro ⟨k, hk⟩
    exact ⟨k, by simp [(commute_X P).mul_pow, hk]⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent (∑ i ∈ Finite.toFinset h, f i)

Tactic:
exact Commute.isNilpotent_sum (fun b _ ↦ hf b) (fun _ _ _ _ ↦ h_comm _ _)

Goal state after:
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 ι
A : Matrix ι ι R
j : ι
⊢ (Fintype.linearCombination R b) (A *ᵥ Pi.single j 1) = ∑ i, A i j • b i

Tactic:
Fintype.linearCombination_apply,

Goal state after:
ι : 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 ι
A : Matrix ι ι R
j : ι
⊢ ∑ i, (A *ᵥ Pi.single j 1) i • b i = ∑ i, A i j • b i
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.ncard = p.spanFinrank

Tactic:
← Nat.cast_inj (R := Cardinal),

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
⊢ ↑p.generators.ncard = ↑p.spanFinrank
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
n : ℤ
⊢ IsIntegral R ↑n

Tactic:
rw [← map_intCast (_ : R →+* B) n]

Goal state after:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
n : ℤ
⊢ IsIntegral R (?m.25 ↑n)

R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
n : ℤ
⊢ R →+* B
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
n : ℤ
⊢ IsIntegral R ↑n

Tactic:
by
  rw [← map_intCast (_ : R →+* B) n]
  exact isIntegral_algebraMap

Goal state after: