mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
⊢ ⊤ ≤ span K (Set.range fun x ↦ _root_.id ↑x)

Tactic:
simpa using

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
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
⊢ span K n = ⊤
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
a b✝ : A
s : Set A
hb✝ : b✝ ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
h_star : ∀ b ∈ s, Commute a (star b)
b : A
hb : b ∈ s ∪ star s
⊢ b ∈ star s → Commute a b

Tactic:
simpa using

Goal state after:
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
a b✝ : A
s : Set A
hb✝ : b✝ ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
h_star : ∀ b ∈ s, Commute a (star b)
b : A
hb : b ∈ s ∪ star s
⊢ star b ∈ s → Commute a b
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ ↑f ⟨c • x, ⋯⟩ = ↑g ⟨c • x, ⋯⟩

Tactic:
rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]

Goal state after:
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
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)

Tactic:
simpa using

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
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
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝¹ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹
b_eq : b = Basis.extend this✝¹
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯
this : span K (Basis.ofVectorSpaceIndex K ↥S) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∀ (v : V), v = 0

Tactic:
simpa using

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∀ (v : V), v = 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
h' : v₀ = 0
⊢ False

Tactic:
by
    simp only [h', ne_eq] at H; exact H rfl

Goal state after:
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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ f y = f x

Tactic:
simpa using

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ f y = f x
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
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ K ∙ v₀
κ : Type v
b : Basis κ K ↥s
⊢ Module.rank K ↥s ≤ 1

Tactic:
simpa using

Goal state after:
case mpr
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
h : s ≤ K ∙ v₀
κ : Type v
b : Basis κ K ↥s
⊢ Module.rank K ↥s ≤ 1
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
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W) → ∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v

Tactic:
· rintro ⟨a, ⟨h, ha⟩⟩
    choose f hf using h
    exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩

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 u_1
inst✝ : Unique ι
b : Basis ι K V
⊢ finrank K V = 1

Tactic:
simpa using

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 u_1
inst✝ : Unique ι
b : Basis ι K V
⊢ finrank K V = 1
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ (f i * s.noncommProd f ⋯).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker

Tactic:
Module.End.mul_eq_comp,

Goal state after:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ (f i ∘ₗ s.noncommProd f ⋯).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K V : Type u
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ #V = #K ^ Module.rank K V

Tactic:
simpa using

Goal state after:
K V : Type u
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ #V = #K ^ Module.rank K V
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
h : Disjoint (f i).ker (((insert i s).erase i).sup fun i ↦ (f i).ker)
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker

Tactic:
simpa using

Goal state after:
case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
h : Disjoint (f i).ker (((insert i s).erase i).sup fun i ↦ (f i).ker)
⊢ Disjoint (f i).ker (⨆ x ∈ s, (f x).ker)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b : FreeAlgebra R X), a + b = b + a

Tactic:
rintro ⟨⟩ ⟨⟩
    exact Quot.sound Rel.add_comm

Goal state after:
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 : V
nz : v ≠ 0
h : finrank K V = 1
⊢ K ∙ v = ⊤

Tactic:
simpa using

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
h : finrank K V = 1
⊢ K ∙ v = ⊤
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
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
⊢ Surjective ⇑(↑K f)

Tactic:
obtain ⟨v, n⟩ := DFunLike.ne_iff.mp w

Goal state after:
K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
v : V
n : f v ≠ 0 v
⊢ Surjective ⇑(↑K f)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)

Tactic:
Module.End.mul_eq_comp,

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)

Tactic:
Module.End.mul_eq_comp,

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ ((f ^ k) ∘ₗ f ^ m).ker
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : Ring T
σ✝ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module R E
F : Type u_5
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module S F
G : Type u_6
inst✝⁵ : AddCommGroup G
inst✝⁴ : Module T G
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
⊢ Disjoint f.domain (mkSpanSingleton x y ⋯).domain

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : Ring T
σ✝ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module R E
F : Type u_5
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module S F
G : Type u_6
inst✝⁵ : AddCommGroup G
inst✝⁴ : Module T G
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
⊢ x ∈ f.domain → x = 0
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
rw [sup_apply _ ⟨x', hx'⟩ ⟨c • x, _⟩, mkSpanSingleton'_apply]

Goal state after:
case hz
E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑⟨x', hx'⟩ + ↑⟨c • x, ?m.146⟩ = ↑⟨x' + c • x, ⋯⟩

E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton x y ⋯).domain
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
simpa using

Goal state after:
E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
c : K
⊢ ↑(f.supSpanSingleton x y hx) ⟨c • x, ⋯⟩ = σ c • y
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r a : R
hr : r ≠ 0
⊢ ¬(C r).IsRoot a

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
r a : R
hr : r ≠ 0
⊢ ¬r = 0
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
simpa using

Goal state after:
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ n.minFacProp (if True then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsLeftCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a % p = b % p)
hle : b < a
⊢ ↑a = ↑b ↔ a % p = b % p

Tactic:
simpa using

Goal state after:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsLeftCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a % p = b % p)
hle : b < a
⊢ ↑a = ↑b ↔ a % p = b % p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
this : (a + c - a) % p = 0
⊢ p ∣ c

Tactic:
simpa using

Goal state after:
case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
this : (a + c - a) % p = 0
⊢ c % p = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ 1 = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ False
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ringChar R ≠ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ¬Subsingleton R
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : ExpChar R q
h : Nat.Prime q
⊢ 0 < q

pp: case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : ExpChar R 1
⊢ 0 < 1

Tactic:
exacts [Nat.Prime.pos h, Nat.one_pos]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1

Tactic:
rintro rfl
    exact expChar_one_of_char_zero R q

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₂

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
⊢ (a₁.coeff.sum fun a b ↦ a₂.coeff.sum fun a_1 b_1 ↦ (b * b_1) • (f a * f a_1)) =
    a₂.coeff.sum fun a c ↦ a₁.coeff.sum fun a_1 c_1 ↦ (c_1 * c) • (f a_1 * f a)
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x ↦ f x - g x) l a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x ↦ f x + -g x) l a
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x ↦ f x - g x) l a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x ↦ f x + -g x) l a
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn (fun x ↦ f x - g x) s a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn (fun x ↦ f x + -g x) s a
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn (fun x ↦ f x - g x) s a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn (fun x ↦ f x + -g x) s a
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
m : M
a : A
⊢ φ₁ (single m a) = φ₂ (single m a)

Tactic:
simpa using

Goal state after:
case single
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
m : M
a : A
⊢ φ₁ (single m a) = φ₂ (single m a)