mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) = fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂)

Tactic:
ext (i | i) (j | j)

Goal state after:
case inl.inl
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : n
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inl i) (Sum.inl j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inl i) (Sum.inl j)

case inl.inr
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : n
j : m
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inl i) (Sum.inr j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inl i) (Sum.inr j)

case inr.inl
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : m
j : n
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inr i) (Sum.inl j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inr i) (Sum.inl j)

case inr.inr
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : m
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inr i) (Sum.inr j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inr i) (Sum.inr j)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) ((leftMulMatrix c) ((algebraMap S T) x) (i, k).2 (j, k').2) (i, k).1 (j, k').1 =
    blockDiagonal (fun x_1 ↦ (leftMulMatrix b) x) (i, k) (j, k')

Tactic:
AlgHom.commutes,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) ((algebraMap S (Matrix n n S)) x (i, k).2 (j, k').2) (i, k).1 (j, k').1 =
    blockDiagonal (fun x_1 ↦ (leftMulMatrix b) x) (i, k) (j, k')
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ smithCoeffs b I hI i ≠ 0

Tactic:
by
  intro hi
  apply Basis.ne_zero (Ideal.selfBasis b I hI) i
  refine Subtype.coe_injective ?_
  simp [hi]

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

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
x y : ↥M
⊢ mk' S (↑x) y * mk' S (↑y) x = 1

Tactic:
← mk'_mul,

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
x y : ↥M
⊢ mk' S (↑x * ↑y) (y * x) = 1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap K₂ L₂) (e ((algebraMap A K₁) r)) / (algebraMap K₂ L₂) (e ((algebraMap A K₁) s)) =
    f ((algebraMap K₁ L₁) ((algebraMap A K₁) r)) / f ((algebraMap K₁ L₁) ((algebraMap A K₁) s))

Tactic:
AlgHom.commutes,

Goal state after:
A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap K₂ L₂) ((algebraMap A K₂) r) / (algebraMap K₂ L₂) ((algebraMap A K₂) s) =
    f ((algebraMap K₁ L₁) ((algebraMap A K₁) r)) / f ((algebraMap K₁ L₁) ((algebraMap A K₁) s))
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap A L₂) r / (algebraMap A L₂) s =
    f ((algebraMap B L₁) ((algebraMap A B) r)) / f ((algebraMap B L₁) ((algebraMap A B) s))

Tactic:
AlgHom.commutes,

Goal state after:
A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap A L₂) r / (algebraMap A L₂) s =
    (algebraMap B L₂) ((algebraMap A B) r) / (algebraMap B L₂) ((algebraMap A B) s)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
⊢ Bijective ⇑(algebraMap R Rₘ)

Tactic:
refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩

Goal state after:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
x : Rₘ
⊢ ∃ a, (algebraMap R Rₘ) a = x
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ s⋆ = s

Tactic:
rw [← star_preimage]
    ext1
    simp [star_trivial]

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ IsStarProjection (q - p) ↔ q * p = p

Tactic:
rw [← star_inj]
  simp [star_mul, hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq,
    sub_iff_mul_eq_left hp hq]

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ resolventSet R a = univ

Tactic:
by
  simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.ofPred_true]

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

Goal state before:
pp: case tmul
R : Type uR
A : Type uA
B : Type uB
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
x : A
y : B
⊢ f (x ⊗ₜ[R] y) = g (x ⊗ₜ[R] y)

Tactic:
simpa [← map_mul] using congr($h₁ x * $h₂ y)

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
hcomm : Commute (↑a) (r • ↑a⁻¹ - 1)
⊢ IsUnit (r • ↑a⁻¹ - 1)

Tactic:
exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)

Tactic:
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x → ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

pp: case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x

Tactic:
· rintro ⟨u, rfl⟩
    exact ⟨equiv.symm u⁻¹.val, by simp⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
r : R
⊢ (algebraMap R C) ((algebraMap R (Unitization R A)) r).toProd.1 + φ ((algebraMap R (Unitization R A)) r).toProd.2 =
    (algebraMap R C) r

Tactic:
simp only [algebraMap_eq_inl, fst_inl, snd_inl, φ.map_zero, add_zero]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1,
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x) →
    ∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x

Tactic:
rintro ⟨y, hy⟩
      refine ⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).injective ?_⟩
      rw [← hy, comm_comp_map_apply, ← Algebra.TensorProduct.comm_symm, AlgEquiv.symm_apply_apply]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ finrank R (Matrix m n M) = card m * card n * finrank R M

Tactic:
simp [finrank]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι → R) = Fintype.card ι

Tactic:
simp [finrank]

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

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
⊢ finrank R (M ⊗[S] M') = finrank R M * finrank S M'

Tactic:
simp [finrank]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ Module.rank R M ≠ 0

Tactic:
← Cardinal.one_le_iff_ne_zero

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ 1 ≤ Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le

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

Goal state before:
pp: R : Type u
ι : Type w
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
inst✝¹ : Finite ι
inst✝ : Nontrivial R
s : Set ι
⊢ finrank R ↥(spanSubset R s) = s.ncard

Tactic:
by
  classical
  have := Fintype.ofFinite ι
  rw [Pi.spanSubset, finrank_span_set_eq_card <| (Pi.basisFun R ι).linearIndepOn _ |>.id_image,
    Set.toFinset_card, Fintype.card_eq_nat_card, Nat.card_coe_set_eq]
  exact Set.ncard_image_of_injective s <| (Pi.basisFun R ι).injective

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
cases nonempty_fintype s

Goal state after:
case inl.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
cases nonempty_fintype s

Goal state after:
case inr.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case left
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ K ∙ v ≠ ⊥

Tactic:
rw [Submodule.ne_bot_iff]
    exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : Subsingleton M
⊢ finrank R M ≤ 0

Tactic:
exact finrank_zero_of_subsingleton.le

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = (σ (Classical.choose ⋯) + σ (Classical.choose ⋯)) • y

Tactic:
← RingHom.map_add,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = σ (Classical.choose ⋯ + Classical.choose ⋯) • y
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
x✝ : V
⊢ x✝ ∈ K ∙ v₀ ↔ x✝ ∈ ⊤

Tactic:
simp [mem_span_singleton, hv₀]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
obtain ⟨s, hs⟩ := Module.Free.exists_basis (R := K) (M := V)

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case pos
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
⊢ S = ⊥

pp: case neg
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
⊢ S = ⊥

Tactic:
· refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_
    rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1
    obtain ⟨h1⟩ := h1
    obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩
    exact ⟨y, congr(Subtype.val $(hy))⟩

Goal state after:
case neg
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
⊢ S = ⊥
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝ : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
⊢ liftFun R X f a = liftFun R X f b

Tactic:
induction h
      · exact (algebraMap R A).map_add _ _
      · exact (algebraMap R A).map_mul _ _
      · apply Algebra.commutes
      · change _ + _ + _ = _ + (_ + _)
        rw [add_assoc]
      · change _ + _ = _ + _
        rw [add_comm]
      · change algebraMap _ _ _ + liftFun R X f _ = liftFun R X f _
        simp
      · change _ * _ * _ = _ * (_ * _)
        rw [mul_assoc]
      · change algebraMap _ _ _ * liftFun R X f _ = liftFun R X f _
        simp
      · change liftFun R X f _ * algebraMap _ _ _ = liftFun R X f _
        simp
      · change _ * (_ + _) = _ * _ + _ * _
        rw [left_distrib]
      · change (_ + _) * _ = _ * _ + _ * _
        rw [right_distrib]
      · change algebraMap _ _ _ * _ = algebraMap _ _ _
        simp
      · change _ * algebraMap _ _ _ = algebraMap _ _ _
        simp
      repeat
        change liftFun R X f _ + liftFun R X f _ = _
        simp only [*]
        rfl
      repeat
        change liftFun R X f _ * liftFun R X f _ = _
        simp only [*]
        rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : ↥(f.supSpanSingleton x y hx).domain
hx' : ↑x' ∈ f.domain
⊢ ↑(f.supSpanSingleton x y hx) x' = ↑f ⟨↑x', hx'⟩

Tactic:
by
  simpa using supSpanSingleton_apply_mk f x y hx x' hx' 0

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp 0 = C (eval 0 p)

Tactic:
rw [← C_0, comp_C]

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
lift a to ℕ using le_of_lt h with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Tactic:
exact ‹p.Prime›.ne_zero

Goal state after: