mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (r • g))) x✝¹) x✝ = ((curry (r • map f g)) x✝¹) x✝

Tactic:
curry_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((TensorProduct.curry (↑R (map f (r • g)))) x✝¹) x✝ = ((TensorProduct.curry (↑R (r • map f g))) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝

Tactic:
curry_apply,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((TensorProduct.curry (↑R (map (b • f) g))) x✝¹) x✝ = ((TensorProduct.curry (↑R (b • map f g))) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p)) = ⊤

Tactic:
eq_top_iff,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⊤ ≤ comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p))
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A ⊥ = ⊥

Tactic:
simp [baseChange_eq_span]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A ⊤ = ⊤

Tactic:
eq_top_iff,

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤ ≤ baseChange A ⊤
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ LinearIndependent R A.col

Tactic:
rw [← Matrix.mulVec_injective_iff]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective A.mulVec
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✝⁵ : Finite m
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₂
M : Matrix m n R
x : M₁
⊢ ⇑(v₂.repr (((toLin v₁ v₂) M) x)) = M *ᵥ ⇑(v₁.repr x)

Tactic:
by
  rw [← toMatrix_mulVec_repr v₁, toMatrix_toLin]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
⊢ f (f.sec 0).1 = 0

Tactic:
by
  rw [LocalizationMap.sec_spec', mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : Monoid R
S : Submonoid R
inst✝⁷ : OreSet S
X : Type u_2
inst✝⁶ : AddMonoid X
inst✝⁵ : DistribMulAction R X
R₀ : Type ?u.16
inst✝⁴ : Monoid R₀
inst✝³ : MulAction R₀ X
inst✝² : MulAction R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x✝ : R₀
⊢ x✝ • 0 = 0

Tactic:
rw [← smul_one_oreDiv_one_smul, smul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
t : R
s : ↥S
ht : t * ↑s ∈ S
⊢ -r /ₒ s = -(t • r) /ₒ ⟨t * ↑s, ht⟩

Tactic:
rw [← smul_neg, ← OreLocalization.expand]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i : Fin (n' + 1)
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') 0) =
    Fin.cons a as 0 • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ 0))

Tactic:
simp only [Fin.cons_zero, Fin.castLE_zero]

Goal state after:
case neg.intro.refine_2.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i : Fin (n' + 1)
⊢ y = a • y'
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = (algebraMap R₀ R) r /ₒ 1 * x

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) =
    (snf.a i • c.sum fun a b ↦ b • snf.bN.repr ⟨↑(snf.bN a), ⋯⟩) i

Tactic:
Subtype.coe_eta,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = (snf.a i • c.sum fun a b ↦ b • snf.bN.repr (snf.bN a)) i
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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : 0 ∈ M
⊢ 0 = 1

Tactic:
by simpa using IsLocalization.map_units S ⟨0, h⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * (b * c) = star a * b * c

Tactic:
simpa only [star_mul, star_star] using congr_arg star (ha.right_assoc (star c) (star b))

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ˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
by_cases h : s ∈ spectrum R a

Goal state after:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) t ∈ I • ⊤

Tactic:
exact t.induction_on (by simp) (by simp +contextual [Submodule.smul_mem_smul])
    (by simp +contextual [add_mem])

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ (1 + ↑(PreQuasiregular.equiv.symm ↑x)) * (1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)) = 1

Tactic:
convert congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A))
          · simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]
            abel
          · simp only [inr_zero, add_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
refine ⟨y, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ y + a + a * y = 0

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ a + y + y * a = 0
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
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • ↑a))

Tactic:
rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

Goal state after:
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
r : R
this : {0} ⊆ spectrum R ↑a
x : IsUnit r
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(x.unit⁻¹ • ↑a))

Tactic:
rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (c • a)

Tactic:
have hunit : IsUnit (c • a) :=
    isUnit_iff_exists.mpr ⟨c⁻¹ • ha.isUnit.unit⁻¹, by simp [(ne_of_lt hc).symm]⟩
  exact hunit.isStrictlyPositive (smul_nonneg hc.le ha.nonneg)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (m x : A), (m • x) • baseChangeHom R A M N = (RingHom.id A) m • x • baseChangeHom R A M N

Tactic:
by simp only [smul_assoc, RingHom.id_apply, forall_true_iff]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T K : Subalgebra R A
⊢ S ≤ centralizer R ↑K ∧ T ≤ centralizer R ↑K ↔ K ≤ centralizer R ↑S ⊓ centralizer R ↑T

Tactic:
le_inf_iff,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T K : Subalgebra R A
⊢ S ≤ centralizer R ↑K ∧ T ≤ centralizer R ↑K ↔ K ≤ centralizer R ↑S ∧ K ≤ centralizer R ↑T
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case 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 A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range → w ∈ centralizer R (⇑includeLeft '' S)

Tactic:
rintro ⟨w, rfl⟩

Goal state after:
case 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 A
inst✝ : Module.Free R B
w : ↥(centralizer R S) ⊗[R] B
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w ∈ centralizer R (⇑includeLeft '' S)
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 : a ≤ b
⊢ IsSelfAdjoint a ↔ IsSelfAdjoint b

Tactic:
replace hab := (sub_nonneg.mpr hab).isSelfAdjoint
  aesop (add simp IsSelfAdjoint)

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 : LinearIndepOn R id s
⊢ #↑↑⟨s, li⟩ ≤ ↑n

Tactic:
exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li

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
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type v'
bN : Basis fst✝ S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst✝¹ * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
← bN.mk_eq_rank'',

Goal state after:
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
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type v'
bN : Basis fst✝ S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst✝¹ * Cardinal.lift.{v, v'} #fst✝
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
⊢ Set.finrank R ∅ = 0

Tactic:
by
  rw [Set.finrank, span_empty, finrank_bot]

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

Goal state before:
pp: case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ (∃ v₀ ∈ s, s ≤ K ∙ v₀) → ∃ v₀, s ≤ K ∙ v₀

Tactic:
rintro ⟨v₀, _, h⟩

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
left✝ : v₀ ∈ s
h : s ≤ K ∙ v₀
⊢ ∃ v₀, s ≤ K ∙ v₀
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ 1
⊢ Module.rank F ↥⊥ ≤ 1

Tactic:
lift_le_one_iff,

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : Module.rank F ↥1 ≤ 1
⊢ Module.rank F ↥⊥ ≤ 1
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod

Tactic:
by
  induction ps using List.reverseRecOn with
  | nil => simp
  | append_singleton ps p ihp =>
    simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
    simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x y : k[G]
⊢ (x * y).coeff.support ⊆ x.coeff.support * y.coeff.support

Tactic:
simp only [MonoidAlgebra.mul_def, coeff_finsuppSum]
  grw [Finsupp.support_sum, biUnion_subset]
  rintro x hx
  grw [Finsupp.support_sum, biUnion_subset]
  exact fun y hy ↦ support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
p2 : 2 ≤ p
m : ℕ
h : m < p → m ∣ p → m = 1
m2 : 2 ≤ m
l : m < p
d : m ∣ p
⊢ 1 < 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩ = ↑l x

Tactic:
symm

Goal state after:
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑l x = ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: ⊢ Prime 2

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: ⊢ Prime 3

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: ⊢ Prime 5

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: ⊢ Prime 7

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: ⊢ Prime 11

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n k : ℕ
h : ¬n < k * k
⊢ 0 < 2

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ 0 < 1

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < 0

Tactic:
decide

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : v ∣ 1
⊢ v = 1

Tactic:
Nat.dvd_one

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : v = 1
⊢ v = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
H : p.natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False

Tactic:
exact LT.lt.false H

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 ≠ 1
p : R[X]
hp : p.Monic
⊢ p ≠ 0

Tactic:
nontriviality R
  exact hp.ne_zero

Goal state after: