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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (congr ((starLinearEquiv R).trans (starLinearEquiv R)) ((starLinearEquiv R).trans (starLinearEquiv R))) x = x

Tactic:
convert! congr($congr_refl_refl x)

Goal state after:
case e'_2.e'_21
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (starLinearEquiv R).trans (starLinearEquiv R) = LinearEquiv.refl R A

case e'_2.e'_22
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (starLinearEquiv R).trans (starLinearEquiv R) = LinearEquiv.refl R B
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x y : ℕ
h : (algebraMap ℕ ℚ≥0) x = (algebraMap ℕ ℚ≥0) y
⊢ ↑1 * x = ↑1 * y

Tactic:
simpa using h

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * IsFractionRing.inv A x = 1

Tactic:
rw [IsFractionRing.inv, dif_neg hx, ←
    IsUnit.mul_left_inj
      (map_units K
        ⟨(sec _ x).1,
          mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
            hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
    one_mul, mul_assoc]
  rw [mk'_spec, ← eq_mk'_iff_mul_eq]
  exact (mk'_sec _ x).symm

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
a c : R
b d : ↥M
⊢ mk (↑d * a + -(↑b * c)) (b * d) = mk (↑d * a - ↑b * c) (b * d)

Tactic:
← sub_eq_add_neg

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
a c : R
b d : ↥M
⊢ mk (↑d * a - ↑b * c) (b * d) = mk (↑d * a - ↑b * c) (b * d)
Module: Mathlib.RingTheory.Localization.Basic

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
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) = mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
by
  rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
    IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ,
    IsScalarTower.algebraMap_apply R Rₘ Sₘ, ← map_mul, mul_comm,
    IsLocalization.mul_mk'_eq_mk'_of_mul]
  exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
have hs₂ : BddAbove s := ⟨n, fun x hx ↦ (hns x hx).le⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
⊢ (∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)) ↔ a * ↑d = ↑b * c

Tactic:
refine ⟨fun ⟨u, hu, h⟩ ↦ ?_,
    fun h ↦ ⟨1, Submonoid.one_mem M, by simpa only [one_mul, mul_comm a] using h⟩⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
⊢ a * ↑d = ↑b * c
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ s⋆ = s

Tactic:
by
    rw [← star_preimage]
    ext1
    simp [star_trivial]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer

Tactic:
simp_rw [centralizer, ← commute_iff_eq]

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, Commute m c} = {c | ∀ m ∈ star s, Commute m c}
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
inst✝ : Nontrivial A
r : R
a : A
⊢ r ∈ σ a ↔ resolvent a r = 0

Tactic:
refine ⟨resolvent_zero_of_mem_spectrum, fun hr ↦ ?_⟩

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial A
r : R
a : A
hr : resolvent a r = 0
⊢ r ∈ σ a
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
⊢ c • a * c⁻¹ • ↑⋯.unit⁻¹ = 1 ∧ c⁻¹ • ↑⋯.unit⁻¹ * c • a = 1

Tactic:
simp [(ne_of_lt hc).symm]

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 : R
⊢ 0 < x ↔ x ≠ 0 ∧ x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
by
  simp [lt_iff_le_and_ne, and_comm, eq_comm, le_iff]

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

Goal state before:
pp: case e'_3.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 B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1,
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x) →
    ∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x

Tactic:
rintro ⟨y, hy⟩

Goal state after:
case e'_3.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 B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
y : ↥(centralizer R S) ⊗[R] A
hy : (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y = (Algebra.TensorProduct.comm R A B) x
⊢ ∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x
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
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : 0 < a
r s : R
hrs : r < s
⊢ r • a < s • a

Tactic:
rw [StarOrderedRing.pos_iff] at ha

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
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r < s
⊢ r • a < s • a
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
⊢ Module.rank R ↥(span R ↑s) ≤ ↑s.card

Tactic:
by
  simpa using rank_span_le (s : Set M)

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

pp: case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
· obtain ⟨⟨s, hs⟩, hs'⟩ := exists_eq_ciSup_of_not_isSuccLimit
      Cardinal.bddAbove_of_small (h.trans (Module.rank_def R M) ▸ not_isSuccLimit_natCast n)
    rw [← Module.rank_def, ← h] at hs'
    have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ natCast_lt_aleph0)
    cases nonempty_fintype s
    refine ⟨s.toFinset, by simpa using hs', by simpa⟩

Goal state after:
case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
⊢ ∃ g, g ∘ₗ f = id

Tactic:
have BC := this.subset_extend (subset_univ _)

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : ⇑f '' B ⊆ this.extend ⋯
⊢ ∃ g, g ∘ₗ f = id
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: 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
φ : F
⊢ ∀ {a : B},
    a ∈ (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier →
      star a ∈ (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier

Tactic:
rintro _ ⟨a, rfl⟩; exact ⟨star a, map_star φ a⟩

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

Goal state before:
pp: A : Type v
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R A
s : NonUnitalStarSubalgebra R A
⊢ Submodule.span R ↑s = s.toSubmodule

Tactic:
simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M) (a : Basis (↑s) R M), ¬s.Finite
h✝ : Subsingleton R
this : Subsingleton M
⊢ finrank R M = 0

Tactic:
exact (h ∅ ⟨LinearEquiv.ofSubsingleton _ _⟩ Set.finite_empty).elim

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
⊢ ∀ (a : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (star a) =
      star (Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ a)

Tactic:
dsimp only [SetLike.coe_sort_coe, NonUnitalStarAlgHom.comp_apply, inclusion_mk, Eq.ndrec,
          id_eq, eq_mpr_eq_cast, ZeroMemClass.coe_zero, AddSubmonoid.mk_add_mk, Set.inclusion_mk,
          MulMemClass.mk_mul_mk, NonUnitalAlgHom.toDistribMulActionHom_eq_coe,
          DistribMulActionHom.toFun_eq_coe, NonUnitalAlgHom.coe_to_distribMulActionHom,
          NonUnitalAlgHom.coe_mk]
        apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => star x)
          (fun _ _ => rfl)
        all_goals simp [map_star]

Goal state after:
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
x y : E
x✝¹ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
x✝ : y ∈ {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⟩
hfy : y ∈ f.domain
hgy : y ∈ g.domain
hy : ↑f ⟨y, hfy⟩ = ↑g ⟨y, hgy⟩
⊢ ↑f ⟨x + y, ⋯⟩ = ↑g ⟨x + y, ⋯⟩

Tactic:
simp_all [← AddMemClass.mk_add_mk, f.map_add, g.map_add]

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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : ↑x' + ↑y' = ↑z'
⊢ fg z' = ↑f x' + ↑g y'

Tactic:
dsimp [fg]

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
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : ↑x' + ↑y' = ↑z'
⊢ ↑f ⟨x z', ⋯⟩ + ↑g ⟨y z', ⋯⟩ = ↑f x' + ↑g y'
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 : V →ₗ[K] V
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
by
  rw [range_eq_top, ker_eq_bot, injective_iff_surjective]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
p : T[X]
g : ℕ → T → R[X]
x : S
⊢ eval₂ f x (p.sum g) = p.sum fun n a ↦ eval₂ f x (g n a)

Tactic:
let T : R[X] →+ S :=
    { toFun := eval₂ f x
      map_zero' := eval₂_zero _ _
      map_add' := fun p q => eval₂_add _ _ }

Goal state after:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
⊢ eval₂ f x (p.sum g) = p.sum fun n a ↦ eval₂ f x (g n a)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ eval x (p * C a) = eval x p * a

Tactic:
rw [eval, eval₂_mul_C'] <;> simp [h]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
⊢ motive a

Tactic:
let s : Subalgebra R (FreeAlgebra R X) :=
    { carrier := {x | motive x}
      mul_mem' := mul _ _
      add_mem' := add _ _
      algebraMap_mem' := grade0 }

Goal state after:
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
⊢ motive a
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
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
by
  rcases c.eq_empty_or_nonempty with rfl | cne
  · simp
  have hdir : DirectedOn (· ≤ ·) (domain '' c) :=
    directedOn_image.2 (hc.mono @(domain_mono.monotone))
  have P : ∀ x : ↥(sSup (domain '' c)), { p : c // (x : E) ∈ p.val.domain } := by
    rintro x
    apply Classical.indefiniteDescription
    have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
    rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this
  set f : ↥(sSup (domain '' c)) → F := fun x => (P x).val.val ⟨x, (P x).property⟩
  have f_eq : ∀ (p : c) (x : ↥(sSup (domain '' c))) (y : p.1.1) (_hxy : (x : E) = y),
      f x = p.1 y := by
    intro p x y hxy
    rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, _hqc, ⟨hxq1, hxq2⟩, ⟨hpq1, hpq2⟩⟩
    exact (hxq2 (y := ⟨y, hpq1 y.2⟩) hxy).trans (hpq2 rfl).symm
  use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_
  · intro x y
    rcases hc (P x).1.1 (P x).1.2 (P y).1.1 (P y).1.2 with ⟨p, hpc, hpx, hpy⟩
    set x' := inclusion hpx.1 ⟨x, (P x).2⟩
    set y' := inclusion hpy.1 ⟨y, (P y).2⟩
    rw [f_eq ⟨p, hpc⟩ x x' rfl, f_eq ⟨p, hpc⟩ y y' rfl, f_eq ⟨p, hpc⟩ (x + y) (x' + y') rfl,
      map_add]
  · intro c x
    rw [f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl, ← map_smulₛₗ]
  · intro p hpc
    refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩
    exact f_eq ⟨p, hpc⟩ _ _ hxy.symm

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

Goal state before:
pp: k : ℕ
⊢ k + 2 ≠ 1

Tactic:
apply Nat.ne_of_gt

Goal state after:
k : ℕ
⊢ 1 < k + 2
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✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
r : R
a : A[M]
a✝ : M
⊢ (r • a).coeff a✝ = ((singleOneRingHom.comp (algebraMap R A)) r * a).coeff a✝

Tactic:
simp [coeff_single_one_mul, Algebra.smul_def]

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ioi a) b

Tactic:
intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ ⟨hx, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx)) g₀
  · exact h₁ self_mem_Ici g₀.le g₀.le

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

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

Tactic:
rw [coeff_mul, Nat.antidiagonal_eq_map]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ Finset.map { toFun := fun i ↦ (i, 1 - i), inj' := ⋯ } (range (1 + 1)), p.coeff x.1 * q.coeff x.2 =
    p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : ↑p.natDegree < q.degree
hq : ¬q = 0
⊢ p.natDegree < q.natDegree

Tactic:
degree_eq_natDegree hq,

Goal state after:
case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : ↑p.natDegree < ↑q.natDegree
hq : ¬q = 0
⊢ p.natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).degree ≤ max p.degree ↑n

Tactic:
rw [degree, support_update]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree ↑n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Tactic:
simpa using h

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

Goal state before:
pp: case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : ↑p.natDegree < q.degree
hq : q ≠ 0
⊢ p.natDegree < q.natDegree

Tactic:
degree_eq_natDegree hq,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : ↑p.natDegree < ↑q.natDegree
hq : q ≠ 0
⊢ p.natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
simp only [ha, (monomial n).map_zero, leadingCoeff_zero]

Goal state after: