mathlib-initiative/mathlib-tactics huggingface dataset:
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:
← inr_smul,

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.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:
← inr_smul,

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R ↑a
x : IsUnit r
⊢ IsQuasiregular (-(↑x.unit⁻¹ • a)) ↔ IsQuasiregular (-↑(↑x.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
⊢ (productMap f g).range = f.range ⊔ g.range

Tactic:
rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : x ≤ y
z : R
⊢ x + z ≤ y + z

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
z : R
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y + z = x + z + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x ≤ y
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint y

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint y
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ star c * a * c ≤ star c * b * c

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), b = a + p
c : R
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), star c * b * c = star c * a * c + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
hc : IsSelfAdjoint c
⊢ c * a * c ≤ c * b * c

Tactic:
simpa only [hc.star_eq] using star_left_conjugate_le_conjugate hab c

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
h : x ≤ y
⊢ star x ≤ star y

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
h : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), star y = star x + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), b = a + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), r • b = r • a + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), s = r + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), s • a = r • a + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
StarOrderedRing.le_iff

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), f y = f x + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
induction hp using AddSubmonoid.closure_induction

Goal state after:
case mem
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ : R
h✝ : x✝ ∈ range fun s ↦ star s * s
⊢ f x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

case zero
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
⊢ f 0 ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

case add
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x p : R
hf : ∀ (r : R), f (star r) = star (f r)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a✝¹ : f x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a✝ : f y✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ f (x✝ + y✝) ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: F : Type u_6
E : Type u_7
R : Type u_8
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : PartialOrder E
inst✝⁸ : StarAddMonoid E
inst✝⁷ : NonUnitalRing R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : SelfAdjointDecompose E
inst✝² : FunLike F E R
inst✝¹ : OrderHomClass F E R
inst✝ : AddMonoidHomClass F E R
f : F
b c : E
hb : 0 ≤ b
hc : 0 ≤ c
ha : IsSelfAdjoint (b - c)
h₁ : f 0 ≤ f b
⊢ IsSelfAdjoint (f (b - c))

Tactic:
have h₂ := OrderHomClass.mono f hc

Goal state after:
F : Type u_6
E : Type u_7
R : Type u_8
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : PartialOrder E
inst✝⁸ : StarAddMonoid E
inst✝⁷ : NonUnitalRing R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : SelfAdjointDecompose E
inst✝² : FunLike F E R
inst✝¹ : OrderHomClass F E R
inst✝ : AddMonoidHomClass F E R
f : F
b c : E
hb : 0 ≤ b
hc : 0 ≤ c
ha : IsSelfAdjoint (b - c)
h₁ : f 0 ≤ f b
h₂ : f 0 ≤ f c
⊢ IsSelfAdjoint (f (b - c))
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 0

Tactic:
intro ⟨s, hs⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : IsAtom W
⊢ ∃ v, v ≠ 0 ∧ W = K ∙ v

pp: case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : ∃ v, v ≠ 0 ∧ W = K ∙ v
⊢ IsAtom W

Tactic:
· obtain ⟨hbot, h⟩ := h
    rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
    refine ⟨v, ⟨hv, ?_⟩⟩
    by_contra heq
    specialize h (span K {v})
    rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
    exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)

Goal state after:
case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : ∃ v, v ≠ 0 ∧ W = K ∙ v
⊢ IsAtom W
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
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 ⋯
⊢ S = ⊤

Tactic:
rw [← b.span_eq, b_eq, Basis.coe_extend, Subtype.range_coe, ← this, ← Submodule.coe_subtype,
    span_image]

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
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 ⋯
⊢ S = Submodule.map S.subtype (span K (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 = S.subtype.range

Tactic:
range_subtype

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
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 = 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
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker

Tactic:
by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa

Goal state after:
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 ↥(Algebra.linearMap F E).range) ≤ lift.{u_2, u_1} (Module.rank F F)
⊢ Module.rank F ↥⊥ ≤ 1

Tactic:
rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_assoc
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ + b✝ + c✝) = liftFun R X f (a✝ + (b✝ + c✝))

Tactic:
change _ + _ + _ = _ + (_ + _)
        rw [add_assoc]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ + c✝) = liftFun R X f (b✝ + c✝)

pp: case add_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

pp: case mul_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
change liftFun R X f _ + liftFun R X f _ = _

Goal state after:
case add_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f a✝¹ + liftFun R X f c✝ = liftFun R X f (b✝ + c✝)

case add_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

case mul_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

pp: case mul_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
change liftFun R X f _ + liftFun R X f _ = _

Goal state after:
case add_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ + liftFun R X f a✝¹ = liftFun R X f (c✝ + b✝)

case mul_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
change liftFun R X f _ + liftFun R X f _ = _

Goal state after:
case mul_compat_left
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.coeff.support
⊢ y ∈ (f * single x r).coeff.support

Tactic:
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.coeff.support ∧ a * x = y := by grind

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
yf : y ∈ f.coeff.support
hy : y * x ∈ image (fun x_1 ↦ x_1 * x) f.coeff.support
⊢ y * x ∈ (f * single x r).coeff.support
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ n.minFacProp (n.minFacAux x✝)

Tactic:
by
    rw [minFacAux]
    by_cases h : n < k * k
    · have pp : Prime n :=
        prime_def_le_sqrt.2
          ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
      simpa only [k, h] using
        ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
    have k2 : 2 ≤ k := by
      subst e
      apply Nat.le_add_left
    simp only [k, h, ↓reduceIte]
    by_cases dk : k ∣ n <;> simp only [k, dk, ↓reduceIte]
    · exact ⟨k2, dk, a⟩
    · refine
        have := minFac_lemma n k h
        minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm])
          fun m m2 d => ?_
      rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml
      · contradiction
      apply (Nat.eq_or_lt_of_le ml).resolve_left
      intro me
      rw [← me, e] at d
      have d' : 2 * (i + 2) ∣ n := d
      have := a _ le_rfl (dvd_of_mul_right_dvd d')
      rw [e] at this
      exact absurd this (by contradiction)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ y, (x, y) ∈ f.graph

Tactic:
use f ⟨x, h⟩
    exact f.mem_graph ⟨x, h⟩

Goal state after: