mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case tmul.tmul
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
⊢ r • (a' ⊗ₜ[R] b' * a ⊗ₜ[R] b) = a' ⊗ₜ[R] b' * r • a ⊗ₜ[R] b

Tactic:
dsimp

Goal state after:
case tmul.tmul
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
⊢ r • (a' * a) ⊗ₜ[R] (b' * b) = a' ⊗ₜ[R] b' * r • a ⊗ₜ[R] b
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.comp includeLeft) a * ((AlgHom.restrictScalars R f).comp includeRight) b =
    (g.comp includeLeft) a * ((AlgHom.restrictScalars R g).comp includeRight) b
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b

Tactic:
dsimp at *

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] 1) * f (1 ⊗ₜ[R] b) = g (a ⊗ₜ[R] 1) * g (1 ⊗ₜ[R] b)
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0} ⊆ σ 0

Tactic:
by simp [Algebra.algebraMap_eq_smul_one, mem_iff]

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

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B) (x_1 y_1 : A ⊗[R] B),
    (x_1 * x ⊗ₜ[R] y) • m = x_1 • x ⊗ₜ[R] y • m →
      (y_1 * x ⊗ₜ[R] y) • m = y_1 • x ⊗ₜ[R] y • m → ((x_1 + y_1) * x ⊗ₜ[R] y) • m = (x_1 + y_1) • x ⊗ₜ[R] y • m

Tactic:
intro a b z w hz hw
      simp only [(· • ·)] at hz hw ⊢
      simp only [map_add, add_mul, LinearMap.add_apply, hz, hw]

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this✝ : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := IsScalarTower.restrictScalars R S C
x✝³ : A
x✝² : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ((LinearMap.mul S (A ⊗[R] B)).compr₂ f)) x✝³) x✝²)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ((LinearMap.mul S C ∘ₗ f).compl₂ f)) x✝³) x✝²)) x✝¹) x✝

Tactic:
dsimp

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this✝ : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := IsScalarTower.restrictScalars R S C
x✝³ : A
x✝² : B
x✝¹ : A
x✝ : B
⊢ f ((x✝³ * x✝¹) ⊗ₜ[R] (x✝² * x✝)) = f (x✝³ ⊗ₜ[R] x✝²) * f (x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a

Tactic:
apply forall_congr' fun hr ↦ ?_

Goal state after:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • ↑a))
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ ((AlgHom.id R S).comp f).range ⊔ ((AlgHom.id R S).comp g).range = f.range ⊔ g.range

Tactic:
AlgHom.id_comp,

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ f.range ⊔ ((AlgHom.id R S).comp g).range = f.range ⊔ g.range
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ (∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p) → x ≤ y

Tactic:
rintro ⟨p, hp, hpxy⟩
      revert x y hpxy
      refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp
      · rintro _ ⟨s, rfl⟩ x y rfl
        exact (h_le_iff _ _).mpr ⟨s, rfl⟩
      · rintro _ _ _ _ ha hb x y rfl
        rw [← add_assoc]
        exact (ha _ _ rfl).trans (hb _ _ rfl)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ 1 = 1

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ 1 = 1
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ 0 = 0

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ 0 = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x + y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x +
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x + y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x +
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
r : R
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ ((algebraMap R ↥(iSup K)) r) =
    (algebraMap R B) r

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
r : R
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ ((algebraMap R ↥(iSup K)) r) =
    (algebraMap R B) r
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
⊢ 0 ≤ u * x * star u ↔ 0 ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩
  obtain ⟨v, hv⟩ := hu.exists_left_inv
  have := by simpa [← mul_assoc] using star_right_conjugate_nonneg h v
  rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this

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

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

Tactic:
by
  rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]

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
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:
← 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.Constructions

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn : Module.rank R M = ↑n
this : Nontrivial R
⊢ M ≃ₗ[R] Fin n → R

Tactic:
have : Cardinal.lift.{u} (n : Cardinal.{v}) = Cardinal.lift.{v} (n : Cardinal.{u}) := by simp

Goal state after:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn : Module.rank R M = ↑n
this✝ : Nontrivial R
this : lift.{u, v} ↑n = lift.{v, u} ↑n
⊢ M ≃ₗ[R] Fin n → R
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✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
      rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this

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✝ : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
⊢ Nonempty (Fintype ι)

Tactic:
by
  rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h

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

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)

Tactic:
dsimp

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f))) (f (hB b)) = hB b
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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

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

Goal state before:
pp: case mpr
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
⊢ Module.rank K V ≤ 1

Tactic:
have h : K ∙ v₀ = ⊤ := by
      ext
      simp [mem_span_singleton, hv₀]

Goal state after:
case mpr
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
h : K ∙ v₀ = ⊤
⊢ Module.rank K V ≤ 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 := ⋯
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₁, hz₁⟩ + ⟨z₂, hz₂⟩)

Tactic:
simp only [coe_add, ← add_assoc]

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₁⟩ + x ⟨z₂, hz₂⟩ + y ⟨z₁, hz₁⟩ + y ⟨z₂, hz₂⟩ = z₁ + z₂
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : f.ker = ⊥
⊢ IsUnit f

Tactic:
rw [ker_eq_bot] at h_inj

Goal state after:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective ⇑f
⊢ IsUnit f
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
⊢ finrank K ↥S = 1

Tactic:
obtain ⟨v : V, hv : v ∈ S, hv_ne : v ≠ 0⟩ := S.ne_bot_iff.mp hS.ne_bot

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ finrank K ↥S = 1
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * (X + ↑n)).comp q = p.comp q * (q + ↑n)

Tactic:
rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]

Goal state after: