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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Ring α

Tactic:
apply e.injective.ring _

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0

case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x : α), e (-x) = -e x

case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n
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 : A
⊢ r ∉ σ a ↔ IsUnit (↑ₐ r - a)

Tactic:
simp [mem_iff]

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
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)

Tactic:
mul_smul_comm r⁻¹ b a

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f)) x) y =
    (((LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)) x) y

Tactic:
congr

Goal state after:
R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f) =
    (LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i)⁻¹ = ↑⋯.unit⁻¹

Tactic:
congr

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ MulEquiv.piUnits hx.unit i = ⋯.unit
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective ⇑φ
x : Unitization R A
⊢ ∀ ⦃a₂ : Unitization R A⦄, (starMap φ) x = (starMap φ) a₂ → x = a₂

Tactic:
y

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective ⇑φ
x y : Unitization R A
⊢ (starMap φ) x = (starMap φ) y → x = 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
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ x + star d = x + d

Tactic:
congr

Goal state after:
case e_a
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ star d = d
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 : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ star c * a * c

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha
  refine AddSubmonoid.closure_induction (fun x hx => ?_)
    (by rw [mul_zero, zero_mul]) (fun x y _ _ hx hy => ?_) ha
  · obtain ⟨x, rfl⟩ := hx
    convert! star_mul_self_nonneg (x * c) using 1
    rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
  · calc
      0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx
      _ ≤ star c * x * c + star c * y * c := by gcongr
      _ ≤ _ := by rw [mul_add, add_mul]

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 : R
⊢ ∀ (y : R), x ≤ y → star x ≤ star y

Tactic:
y

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
⊢ x ≤ y → star x ≤ star y
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p

Tactic:
← unop_le_unop,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ unop x ≤ unop y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

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

Tactic:
rw [Set.iUnionLift_mk]

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

Goal state before:
pp: case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
⊢ K ∙ v ≤ T

Tactic:
change span K {v} ≤ T

Goal state after:
case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
⊢ K ∙ v ≤ T
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: case mk.mk
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
toNonUnitalSubalgebra✝¹ : NonUnitalSubalgebra R A
star_mem'✝¹ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝¹.carrier → star a ∈ toNonUnitalSubalgebra✝¹.carrier
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝¹, star_mem' := star_mem'✝¹ } =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
toNonUnitalSubalgebra✝¹ : NonUnitalSubalgebra R A
star_mem'✝¹ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝¹.carrier → star a ∈ toNonUnitalSubalgebra✝¹.carrier
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ toNonUnitalSubalgebra✝¹ = toNonUnitalSubalgebra✝
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
⊢ ↑v ∈ s

Tactic:
refine ⟨v, ?_, by simp⟩

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
⊢ v ∈ Set.range ⇑b₁
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
f_dom : Submodule R E
f g : ↥f_dom →ₛₗ[σ] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := g }

Tactic:
congr

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
f_dom : Submodule R E
f g : ↥f_dom →ₛₗ[σ] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ f = g
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
f g : E →ₛₗ.[σ] F
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ ↑f x = ↑f y

Tactic:
congr

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
f g : E →ₛₗ.[σ] F
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ x = y
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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = ↑(mkSpanSingleton' x y H) ⟨1 • x, ?m.71⟩

Tactic:
congr

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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ x = 1 • 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
inst✝ : Free K V
κ : Type v
b : Basis κ K V
⊢ (∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v) → Module.rank K V ≤ 1

Tactic:
rintro ⟨v₀, hv₀⟩

Goal state after:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
⊢ Module.rank K V ≤ 1
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
v : V
hv : v ≠ 0
⊢ 0 < finrank K ↥(K ∙ v)

Tactic:
finrank_pos_iff

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Nontrivial ↥(K ∙ v)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R✝ : Type u_1
X : Type u_2
inst✝⁷ : CommSemiring R✝
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ (algebraMap S A) (r • s) • x = ((algebraMap R A) r • (algebraMap S A) s) • x

Tactic:
congr

Goal state after:
case e_a
R✝ : Type u_1
X : Type u_2
inst✝⁷ : CommSemiring R✝
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ (algebraMap S A) (r • s) = (algebraMap R A) r • (algebraMap S A) s
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
⊢ eval₂ f x 1 = 1

Tactic:
← C_1,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (C 1) = 1
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
exact mul_eq_zero_of_right (p.eval₂ f x) hq

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
x✝ : X
⊢ (⇑((lift R) f) ∘ ι R) x✝ = f x✝

Tactic:
Function.comp_apply,

Goal state after:
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
x✝ : X
⊢ ((lift R) f) (ι R x✝) = f x✝
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
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
p : ↑c
x : ↥(sSup (domain '' c))
⊢ ∀ (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y

Tactic:
y

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
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
p : ↑c
x : ↥(sSup (domain '' c))
y : ↥(↑p).domain
⊢ ↑x = ↑y → f x = ↑↑p y
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x : ↥(sSup (domain '' c))
⊢ ∀ (y : ↥(sSup (domain '' c))), f (x + y) = f x + f y

Tactic:
y

Goal state after:
case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
⊢ f (x + y) = f x + f y
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp 1 = C (eval 1 p)

Tactic:
← C_1,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp (C 1) = C (eval 1 p)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ comp 1 p = 1

Tactic:
← C_1,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (C 1).comp p = C 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)

Tactic:
refine
      minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)

Goal state after:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find ⋯ = 0
⊢ ↑(x % Nat.find ⋯) = 0

Tactic:
by
                    rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                      Nat.cast_mul,
                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
                      zero_mul, add_zero] at H1

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n / n.minFac

Tactic:
congr

Goal state after:
case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n

case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n.minFac
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ ringExpChar R = 1

Tactic:
have := CharP.ofCharZero R

Goal state after:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ ringExpChar R = 1
Module: Mathlib.Algebra.CharP.Defs

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

Tactic:
constructor
  · rintro rfl
    exact char_zero_of_expChar_one R p
  · rintro rfl
    exact expChar_one_of_char_zero R q

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
hf : ∀ (m : ↥f.domain), f.toFun m = 0 → m = 0
z : ↥f.domain
hz : ↑f z = 0
⊢ (0, ↑z).2 = 0

Tactic:
simp [hf z hz]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
rcases p with ⟨⟩
  rcases q with ⟨⟩
  simp_rw [← ofFinsupp_add, coeff]
  exact Finsupp.add_apply _ _ _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #{k, m, n} = 3

Tactic:
card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #{m, n} + 1 = 3
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
by
  rw [sub_eq_add_neg, ← supDegree_neg (f := g)]; apply supDegree_add_le

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ ((X + 1) ^ n).coeff k = ↑(n.choose k)

Tactic:
← C_1,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ ((X + C 1) ^ n).coeff k = ↑(n.choose k)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hpq : p.degree = q.degree
⊢ p.natDegree = q.natDegree

Tactic:
simp [natDegree, hpq]

Goal state after: