mathlib-initiative/mathlib-tactics huggingface dataset:
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 : R
m : ↥M
⊢ mk' S (x * 1) m = mk' S x m

Tactic:
mul_one

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 : R
m : ↥M
⊢ mk' S x m = mk' S x m
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₁ x₂ : R
y₁ y₂ : ↥M
⊢ (mk' S x₁ y₁ + mk' S x₂ y₂) * (algebraMap R S) ↑(y₁ * y₂) = (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁)

Tactic:
rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
          mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
          mk'_add_eq_iff_add_mul_eq_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₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submonoid R
hM : Algebra.algebraMapSubmonoid S M ≤ IsUnit.submonoid S
h : Bijective ⇑(algebraMap R S)
y : S
⊢ ∃ x, y * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
obtain ⟨x, rfl⟩ := h.surjective y

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submonoid R
hM : Algebra.algebraMapSubmonoid S M ≤ IsUnit.submonoid S
h : Bijective ⇑(algebraMap R S)
x : R
⊢ ∃ x_1, (algebraMap R S) x * (algebraMap R S) ↑x_1.2 = (algebraMap R S) x_1.1
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
this : Subalgebra.map (IsScalarTower.toAlgHom R A B) (adjoin R s) = Subalgebra.map (IsScalarTower.toAlgHom R A B) ⊤
⊢ Subalgebra.restrictScalars R (adjoin A t) = adjoin R (⇑(algebraMap A B) '' s ∪ t)

Tactic:
rw [Algebra.map_top, AlgHom.map_adjoin, IsScalarTower.coe_toAlgHom'] at this

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
this : adjoin R (⇑(algebraMap A B) '' s) = (IsScalarTower.toAlgHom R A B).range
⊢ Subalgebra.restrictScalars R (adjoin A t) = adjoin R (⇑(algebraMap A B) '' s ∪ t)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m * 1

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case e_a
R✝ : Type u_1
inst✝²⁸ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝²⁷ : CommRing S✝
inst✝²⁶ : Algebra R✝ S✝
P : Type u_3
inst✝²⁵ : CommRing P
A✝ : Type u_4
inst✝²⁴ : CommRing A✝
K✝ : Type u_5
B✝ : Type u_6
inst✝²³ : CommRing B✝
inst✝²² : IsDomain B✝
inst✝²¹ : Field K✝
L✝ : Type u_7
inst✝²⁰ : Field L✝
inst✝¹⁹ : Algebra A✝ K✝
inst✝¹⁸ : IsFractionRing A✝ K✝
g✝ : A✝ →+* L✝
R : Type u_8
S : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
h : IsFractionRing R S
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁴ : Group G
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A L
inst✝³ : IsFractionRing A K
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
this : MulSemiringAction G L := mulSemiringAction G B L
g : G
b : B
x : L
⊢ g • (algebraMap B L) b = (algebraMap B L) (g • b)

Tactic:
apply ringEquivOfRingEquiv_algebraMap

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
K : Type u_5
inst✝ : DecidableEq R
x y : FractionRing R
⊢ Decidable (x = y)

Tactic:
apply Localization.recOnSubsingleton₂ x y (r := fun x y ↦ Decidable (x = y))

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
K : Type u_5
inst✝ : DecidableEq R
x y : FractionRing R
⊢ (a c : R) → (b d : ↥R⁰) → Decidable (Localization.mk a b = Localization.mk c d)
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
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * 1) = (algebraMap R Rₘ) r

Tactic:
mul_one

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
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) r = (algebraMap R Rₘ) r
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x✝ y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x✝ = (lift (LinearMap.mul R A)) y
x : A ⊗[R] A
⊢ ∃ a, x = a ⊗ₜ[R] 1

Tactic:
induction x using TensorProduct.induction_on with

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ⊆ s.centralizer ∩ star s.centralizer ∧ star s ⊆ s.centralizer ∩ star s.centralizer

Tactic:
subset_inter_iff,

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ star s ⊆ s.centralizer ∧ star s ⊆ star s.centralizer
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
a : A
b : B
this : f ((a * 1) ⊗ₜ[R] b) = g ((a * 1) ⊗ₜ[R] b)
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b

Tactic:
mul_one

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
a : A
b : B
this : f (a ⊗ₜ[R] b) = g (a ⊗ₜ[R] b)
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b
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)
⊢ r • 1 - ↑a * 1 = r • 1 - ↑a

Tactic:
mul_one

Goal state after:
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)
⊢ r • 1 - ↑a = r • 1 - ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ spectrum R ↑a ∪ {0} = quasispectrum R a

Tactic:
quasispectrum_eq_spectrum_inr' R S

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ spectrum R ↑a ∪ {0} = spectrum R ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
⊢ quasispectrum R a = ⋃ i, quasispectrum R (a i)

Tactic:
by
  ext r
  simp only [quasispectrum, Set.mem_ofPred_eq, Set.mem_iUnion]
  by_cases hr : IsUnit r
  · lift r to Rˣ using hr with r' hr'
    simp [isQuasiregular_pi_iff]
  · simp [hr]

Goal state after:
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
x y : Unitization R A
⊢ (algebraMap R C) (x + y).toProd.1 + φ (x + y).toProd.2 =
    (algebraMap R C) x.toProd.1 + φ x.toProd.2 + ((algebraMap R C) y.toProd.1 + φ y.toProd.2)

Tactic:
by
    induction x with
    | inl_add_inr =>
      induction y with
      | inl_add_inr =>
        simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr,
          zero_add, φ.map_add]
        rw [add_add_add_comm]

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] (y * 1) = x ⊗ₜ[R] y

Tactic:
mul_one

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y = x ⊗ₜ[R] y
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ star x + star d = x + d

Tactic:
hx.star_eq

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ x + star d = x + d
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mp
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 A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : ∑ i ∈ b.support, (x * b i) ⊗ₜ[R] ℬ i = ∑ i ∈ b.support, (b i * x) ⊗ₜ[R] ℬ i
⊢ ((x • b).sum fun i ↦ ⇑((TensorProduct.mk R A B).flip (ℬ i))) =
    (mapRange (fun x_1 ↦ x_1 * x) ⋯ b).sum fun i ↦ ⇑((TensorProduct.mk R A B).flip (ℬ i))

Tactic:
sum_of_support_subset (s := b.support) (hs := Finsupp.support_smul) (h := by simp),

Goal state after:
case mp
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 A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : ∑ i ∈ b.support, (x * b i) ⊗ₜ[R] ℬ i = ∑ i ∈ b.support, (b i * x) ⊗ₜ[R] ℬ i
⊢ ∑ x_1 ∈ b.support, ((TensorProduct.mk R A B).flip (ℬ x_1)) ((x • b) x_1) =
    (mapRange (fun x_1 ↦ x_1 * x) ⋯ b).sum fun i ↦ ⇑((TensorProduct.mk R A B).flip (ℬ i))
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : IsSelfAdjoint (b - a)
⊢ IsSelfAdjoint a ↔ IsSelfAdjoint b

Tactic:
aesop (add simp IsSelfAdjoint)

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x * 1
⊢ 0 ≤ x

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x
⊢ 0 ≤ x
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : 0 ≤ a
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a

Tactic:
by
    rw [StarOrderedRing.nonneg_iff] at ha
    rw [StarOrderedRing.le_iff] at hrs ⊢
    obtain ⟨r, hr, rfl⟩ := hrs
    exact ⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)

Tactic:
by
  rw [rank_matrix, lift_mul, lift_umax.{v, u}]

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

Goal state before:
pp: R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ ↑(Fintype.card η) * 1 = ↑(Fintype.card η)

Tactic:
mul_one

Goal state after:
R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ ↑(Fintype.card η) = ↑(Fintype.card η)
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n

Tactic:
rw [← Finset.card_map (Embedding.subtype (· ∈ s))]

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ (Finset.map (Embedding.subtype fun x ↦ x ∈ s) t).card ≤ n
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✝ : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : #ι < ℵ₀
⊢ Nonempty (Fintype ι)

Tactic:
Cardinal.lt_aleph0_iff_fintype

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Nonempty (Fintype ι)
⊢ Nonempty (Fintype ι)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ V ↑i ≠ ⊥

Tactic:
exact i.prop

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

Goal state before:
pp: R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : #{ i // p i ≠ ⊥ } < ℵ₀
⊢ Fintype { i // p i ≠ ⊥ }

Tactic:
Cardinal.lt_aleph0_iff_fintype

Goal state after:
R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : Nonempty (Fintype { i // p i ≠ ⊥ })
⊢ Fintype { i // p i ≠ ⊥ }
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
this : ∀ (t : Set A), NonUnitalAlgebra.adjoin R (star t) ≤ star (NonUnitalAlgebra.adjoin R t)
⊢ star (NonUnitalAlgebra.adjoin R s) ≤ NonUnitalAlgebra.adjoin R (star s)

Tactic:
simpa only [star_star] using NonUnitalSubalgebra.star_mono (this (star s))

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i

Tactic:
set n := insert v s

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i
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
inst✝ : Free R M
h : ∀ (s : Set M) (a : Basis (↑s) R M), ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
⊢ finrank R M = 0

Tactic:
have := Set.Infinite.to_subtype (h _ b)

Goal state after:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M) (a : Basis (↑s) R M), ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
this : Infinite ↑w✝
⊢ finrank R M = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
w : V
⊢ (fun f ↦ f default • v) ((fun w ↦ Finsupp.single default ((b.repr w) default / (b.repr v) default)) w) = w

Tactic:
apply_fun b.repr using b.repr.toEquiv.injective

Goal state after:
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
w : V
⊢ b.repr ((fun f ↦ f default • v) ((fun w ↦ Finsupp.single default ((b.repr w) default / (b.repr v) default)) w)) =
    b.repr w
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f * 1
⊢ g * f = 1

Tactic:
mul_one

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ x ⟨z₁, hz₁⟩ + x ⟨z₂, hz₂⟩ + y ⟨z₁, hz₁⟩ + y ⟨z₂, hz₂⟩ = z₁ + z₂

Tactic:
add_right_comm (x _),

Goal state after:
case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ x ⟨z₁, hz₁⟩ + y ⟨z₁, hz₁⟩ + x ⟨z₂, hz₂⟩ + y ⟨z₂, hz₂⟩ = z₁ + z₂