mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s),
      x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
· exact fun r x _ hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r hx

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
⊢ Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

Tactic:
have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.rfl
  simp only [← this, SetLike.coe_subset_coe, adjoin_le_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ

Tactic:
rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]

Goal state after:
Module: Mathlib.Data.Finite.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α ⊕ β)

Tactic:
by
  have := Fintype.ofFinite α
  have := Fintype.ofFinite β
  infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
by_cases ha : IsUnit a
  · obtain ⟨u, rfl⟩ := ha
    rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
  rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁸ : Add A
inst✝⁷ : Add B
inst✝⁶ : Mul A
inst✝⁵ : Mul B
inst✝⁴ : Star A
inst✝³ : Star B
inst✝² : Add C
inst✝¹ : Mul C
inst✝ : Star C
f g : A ≃⋆+* B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
    rcases g with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
    congr

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (Set.range (⇑N.subtype ∘ ⇑b))

Tactic:
Set.range_comp,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (⇑N.subtype '' Set.range ⇑b)
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (Set.range (⇑N.subtype ∘ ⇑b))

Tactic:
Set.range_comp,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (⇑N.subtype '' Set.range ⇑b)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j

pp: case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j

Tactic:
· simp [h]

Goal state after:
case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
⊢ ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin = f

Tactic:
apply (Pi.basisFun R n).ext
    intro j; ext i
    simp only [Pi.basisFun_apply, Matrix.mulVec_single_one, col_apply,
      Matrix.mulVecLin_apply, of_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
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
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ (toMatrix v₁ v₃) ((toLin v₁ v₃) (A * B)) = (toMatrix v₁ v₃) ((toLin v₂ v₃) A ∘ₗ (toLin v₁ v₂) B)

Tactic:
LinearMap.toMatrix_comp v₁ v₂ v₃

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
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
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ (toMatrix v₁ v₃) ((toLin v₁ v₃) (A * B)) = (toMatrix v₂ v₃) ((toLin v₂ v₃) A) * (toMatrix v₁ v₂) ((toLin v₁ v₂) B)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) (x + y)) = (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y)

Tactic:
by
    rw [map_add, map_add]

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

Goal state before:
pp: case pos
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
h : (i, k).2 = (j, k').2
⊢ (leftMulMatrix b) ((algebraMap S S) x) (i, k).1 (j, k').1 = (leftMulMatrix b) x (i, k).1 (j, k').1

Tactic:
simp only at h

Goal state after:
case pos
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
h : k = k'
⊢ (leftMulMatrix b) ((algebraMap S S) x) (i, k).1 (j, k').1 = (leftMulMatrix b) x (i, k).1 (j, k').1
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case neg
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
h : ¬(i, k).2 = (j, k').2
⊢ (leftMulMatrix b) 0 (i, k).1 (j, k').1 = 0

Tactic:
simp only at h

Goal state after:
case neg
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
h : ¬k = k'
⊢ (leftMulMatrix b) 0 (i, k).1 (j, k').1 = 0
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁ = ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₂ ↔
    w + g ↑y * z₁ = g ↑y * z₂

Tactic:
IsUnit.coe_liftRight

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ((↑g).domRestrict M) y * z₁ = ((↑g).domRestrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : (Algebra.ofId R S) x = (Algebra.ofId R S) y
⊢ x = y

Tactic:
obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : (Algebra.ofId R S) x = (Algebra.ofId R S) y
c : ↥M
eq : ↑c * x = ↑c * y
⊢ x = y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inl
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
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx : z * (algebraMap ℤ ℚ) ↑(x1, x2).2 = (algebraMap ℤ ℚ) (x1, x2).1
hx2 : ↑x2 < 0
⊢ ∃ x, z * (algebraMap ℤ ℚ) ↑x.2 = (algebraMap ℤ ℚ) x.1

Tactic:
exact ⟨⟨-x1, ⟨-x2.val, by simpa using hx2⟩⟩, by simpa using hx⟩

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

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ closure (Set.range (⇑(algebraMap L' E) ∘ ⇑i) ∪ S) = closure (Set.range ⇑(algebraMap L' E) ∪ S)

Tactic:
Set.range_comp,

Goal state after:
F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ closure (⇑(algebraMap L' E) '' Set.range ⇑i ∪ S) = closure (Set.range ⇑(algebraMap L' E) ∪ S)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
obtain ⟨n, f, hf⟩ := @Module.Finite.exists_fin R M _ _ _ _
  let s := { m : ℕ | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤ }
  have hns : ∀ x ∈ s, x < n := by
    refine fun x hx ↦ lt_iff_not_ge.mpr fun e ↦ ?_
    have : (Fin.val ⁻¹' Set.Iio x : Set (Fin n)) = Set.univ := by ext y; simpa using y.2.trans_le e
    simp [s, this, hf] at hx
  have hs₁ : s.Nonempty := ⟨0, by simp [s]⟩
  have hs₂ : BddAbove s := ⟨n, fun x hx ↦ (hns x hx).le⟩
  have hs := Nat.sSup_mem hs₁ hs₂
  refine ⟨_, hs, ⟨⟨Submodule.mkQ _ (f ⟨_, hns _ hs⟩), ?_⟩⟩⟩
  have := not_not.mp (notMem_of_csSup_lt (Order.lt_succ _) hs₂)
  rw [← Set.image_singleton, ← Submodule.map_span,
    ← (Submodule.comap_injective_of_surjective (Submodule.mkQ_surjective _)).eq_iff,
    Submodule.comap_map_eq, Submodule.ker_mkQ, Submodule.comap_top, ← this, ← Submodule.span_union,
    Order.Iio_succ_eq_insert (sSup s), ← Set.union_singleton, Set.preimage_union, Set.image_union,
    ← @Set.image_singleton _ _ f, Set.union_comm]
  congr!
  ext
  simp [Fin.ext_iff]

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y : A ⧸ R'
⊢ x ⊗ₜ[R] y = 0

Tactic:
obtain ⟨x, rfl⟩ := R'.mkQ_surjective x

Goal state after:
case tmul
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
y : A ⧸ R'
x : A
⊢ R'.mkQ x ⊗ₜ[R] y = 0
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : Module.Finite K ↥E1
inst✝ : Module.Finite K ↥E2
⊢ Module.Finite K ↥(E1 ⊔ E2)

Tactic:
rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : Module.Finite K ↥E1
inst✝ : Module.Finite K ↥E2
⊢ Module.Finite K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m

Tactic:
intro a m

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
⊢ 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
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 b c : A
h₁ : (↑ₐ r - a) * b = 1
h₂ : c * (↑ₐ r - a) = 1
⊢ b * (↑ₐ r - a) = 1

Tactic:
by rwa [← left_inv_eq_right_inv h₂ h₁]

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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a → x ∈ r • σ a

pp: case mpr
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ r • σ a → r⁻¹ • x ∈ σ a

Tactic:
· exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩

Goal state after:
case mpr
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ r • σ a → r⁻¹ • x ∈ σ a
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3
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✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y x₁ x₂ : A ⊗[R] B
⊢ x₁ * y = y * x₁ → x₂ * y = y * x₂ → (x₁ + x₂) * y = y * (x₁ + x₂)

Tactic:
h₁

Goal state after:
case refine_3
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✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y x₁ x₂ : A ⊗[R] B
h₁ : x₁ * y = y * x₁
⊢ x₂ * y = y * x₂ → (x₁ + x₂) * y = y * (x₁ + x₂)
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

pp: case refine_3.refine_3
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 y : A ⊗[R] B),
    (∀ (x_1 y : A ⊗[R] B),
        (x_1 * x) • m = x_1 • x • m → (y * x) • m = y • x • m → ((x_1 + y) * x) • m = (x_1 + y) • x • m) →
      (∀ (x y_1 : A ⊗[R] B),
          (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m) →
        ∀ (x_1 y_1 : A ⊗[R] B),
          (x_1 * (x + y)) • m = x_1 • (x + y) • m →
            (y_1 * (x + y)) • m = y_1 • (x + y) • m → ((x_1 + y_1) * (x + y)) • m = (x_1 + y_1) • (x + 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:
case refine_3.refine_3
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 y : A ⊗[R] B),
    (∀ (x_1 y : A ⊗[R] B),
        (x_1 * x) • m = x_1 • x • m → (y * x) • m = y • x • m → ((x_1 + y) * x) • m = (x_1 + y) • x • m) →
      (∀ (x y_1 : A ⊗[R] B),
          (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m) →
        ∀ (x_1 y_1 : A ⊗[R] B),
          (x_1 * (x + y)) • m = x_1 • (x + y) • m →
            (y_1 * (x + y)) • m = y_1 • (x + y) • m → ((x_1 + y_1) * (x + y)) • m = (x_1 + y_1) • (x + y) • m
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case e'_4
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 b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Tactic:
· rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]
    all_goals exact fun _ ↦ quasispectrum.not_isUnit_mem _

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x = y
⊢ star x < star y ↔ x < y

pp: case neg
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : ¬x = y
⊢ star x < star y ↔ x < y

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : ¬x = y
⊢ star x < star y ↔ x < y
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case hbc
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀

Tactic:
· rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
    apply Cardinal.natCast_lt_aleph0

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
⊢ Fintype { i // p i ≠ ⊥ }

Tactic:
suffices #{ i // p i ≠ ⊥ } < (ℵ₀ : Cardinal.{w}) by
    rw [Cardinal.lt_aleph0_iff_fintype] at this
    exact this.some
  refine lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_
  simp [Cardinal.natCast_lt_aleph0]

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

Goal state before:
pp: case pos
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
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : i = j
⊢ f (b j) = (f (b i) • b.coord i) (b j)

pp: case neg
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
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ f (b j) = (f (b i) • b.coord i) (b j)

Tactic:
· simp [h]

Goal state after:
case neg
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
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ f (b j) = (f (b i) • b.coord i) (b j)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ Module.rank R M = 1

Tactic:
rank_eq_card_basis b,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ ↑(Fintype.card PUnit.{u + 1}) = 1