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

Goal state before:
pp: case right
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ (toModule S (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i ↦
        AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
      AlgebraTensorModule.lift
        (toModule S ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₁ ↦
          (toModule R ι₂ (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₂ ↦
              (AlgebraTensorModule.curry (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))).flip).flip) =
    LinearMap.id

Tactic:
ext i₁ i₂ x₁ x₂ : 5

Goal state after:
case right
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
i₁ : ι₁
i₂ : M₁ i₁
x₁ : ι₂
x₂ : M₂ x₁
⊢ ((AlgebraTensorModule.curry
              ((toModule S (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i ↦
                  AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
                AlgebraTensorModule.lift
                  (toModule S ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₁ ↦
                    (toModule R ι₂ (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₂ ↦
                        (AlgebraTensorModule.curry
                            (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))).flip).flip)) ∘ₗ
            lof S ι₁ M₁ i₁)
          i₂ ∘ₗ
        lof R ι₂ M₂ x₁)
      x₂ =
    ((AlgebraTensorModule.curry LinearMap.id ∘ₗ lof S ι₁ M₁ i₁) i₂ ∘ₗ lof R ι₂ M₂ x₁) x₂
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
P : Type v
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
⊢ Projective R P

Tactic:
refine of_lifting_property'' (fun p hp ↦ ?_)

Goal state after:
R : Type u
inst✝³ : Semiring R
P : Type v
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
⊢ ∃ h, p ∘ₗ h = LinearMap.id
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
P : Type v
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
⊢ Projective R P

Tactic:
refine of_lifting_property'' (fun p hp ↦ ?_)

Goal state after:
R : Type u
inst✝³ : Ring R
P : Type v
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
⊢ ∃ h, p ∘ₗ h = LinearMap.id
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((w i)⁻¹ • e.coord i) (e j)

Tactic:
trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)

Goal state after:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j)

ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j) = ((w i)⁻¹ • e.coord i) (e j)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
⊢ (diagonal d).toBlock p p = diagonal fun i ↦ d ↑i

Tactic:
ext i j
  by_cases h : i = j
  · simp [h]
  · simp [h, Subtype.val_injective.ne h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ Mᵀ.updateRow j c i✝ j✝ = (M.updateCol j c)ᵀ i✝ j✝

Tactic:
rw [transpose_apply, updateRow_apply, updateCol_apply]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ (if i✝ = j then c j✝ else Mᵀ i✝ j✝) = if i✝ = j then c j✝ else M j✝ i✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ Mᵀ.updateCol i b i✝ j✝ = (M.updateRow i b)ᵀ i✝ j✝

Tactic:
rw [transpose_apply, updateRow_apply, updateCol_apply]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ (if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
y : A ⊗[R] M
hy : y ∈ baseChange A p
⊢ ∃ x, ↑((toBaseChange A p) x) = y

Tactic:
obtain ⟨x, hx⟩ := toBaseChange_surjective A p ⟨y, hy⟩

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
y : A ⊗[R] M
hy : y ∈ baseChange A p
x : A ⊗[R] ↥p
hx : (toBaseChange A p) x = ⟨y, hy⟩
⊢ ∃ x, ↑((toBaseChange A p) x) = y
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
x : K
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simpa only [Set.mem_iInter] using! Set.ext_iff.1 (coe_sInf S) x

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ (LinearMap.single R (fun i ↦ R) x) 1 ᵥ* M) = span R (Set.range M.row)

Tactic:
LinearMap.single,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ { toFun := Pi.single x, map_add' := ⋯, map_smul' := ⋯ } 1 ᵥ* M) = span R (Set.range M.row)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ Function.Injective M.mulVec ↔ LinearIndependent R M.col

Tactic:
change Function.Injective (fun x ↦ _) ↔ _

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ (Function.Injective fun x ↦ M *ᵥ x) ↔ LinearIndependent R M.col
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
⊢ ∀ (ht : t * ↑s ∈ R⁰),
    (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, ht⟩ /ₒ ⟨t • r, ⋯⟩

Tactic:
hst

Goal state after:
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) (f * g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
rw [Module.End.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: A : Type u_3
inst✝ : Semiring A
⊢ (∀ (n : ℕ), IsDedekindFiniteMonoid (End A (Fin n → A))) ↔
    ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f

Tactic:
isDedekindFiniteMonoid_iff

Goal state after:
A : Type u_3
inst✝ : Semiring A
⊢ (∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) ↔
    ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
x : R
eq : z = (algebraMap R K) x / (algebraMap R K) 0
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1

Tactic:
obtain rfl : z = 0 := by simpa using eq
      exact ⟨(0, 1), by simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ ∃ x, a * (algebraMap S₁ T) ↑x.2 = (algebraMap S₁ T) x.1

Tactic:
use ⟨algebraMap R S₁ z * hunit.unit⁻¹, ⟨algebraMap R S₁ n, n, hn, rfl⟩⟩

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₁ T) ↑((algebraMap R S₁) z * ↑hunit.unit⁻¹, ⟨(algebraMap R S₁) n, ⋯⟩).2 =
    (algebraMap S₁ T) ((algebraMap R S₁) z * ↑hunit.unit⁻¹, ⟨(algebraMap R S₁) n, ⋯⟩).1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: G : Type u_10
B : Type u_12
L : Type u_14
inst✝⁸ : Group G
inst✝⁷ : CommRing B
inst✝⁶ : MulSemiringAction G B
inst✝⁵ : Field L
inst✝⁴ : Algebra B L
inst✝³ : IsFractionRing B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : FaithfulSMul G B
m₁✝ m₂✝ : G
h : ∀ (a : L), m₁✝ • a = m₂✝ • a
x : ?m.65 h
⊢ m₁✝ • x = m₂✝ • x

Tactic:
simpa [← algebraMap.coe_smul'] using h (algebraMap B L x)

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
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
have hs₁ : s.Nonempty := ⟨0, by simp [s]⟩

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
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ ∃ a, u ⊗ₜ[R] v = a ⊗ₜ[R] 1

Tactic:
use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
⊢ Sort ?u.13

Tactic:
by
    let add := Equiv.add e
    let mul := Equiv.mul e
    exact α ≃+* β

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddMonoidWithOne β
⊢ e (e.invFun ↑0) = e 0

Tactic:
by simp [zero_def]

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}

Tactic:
suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0} from
    Set.eq_of_subset_of_subset (h a b) (h b a)
  rintro _ _ k ⟨k_mem, k_ne⟩
  change ((Units.mk0 k k_ne) : 𝕜) ∈ _ at k_mem
  exact ⟨unit_mem_mul_comm.mp k_mem, k_ne⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
x✝² x✝¹ x✝ : Unitization R A
⊢ ((x✝² + x✝¹) * x✝).toProd.2 = (x✝² * x✝ + x✝¹ * x✝).toProd.2

Tactic:
by
      simp [smul_add, add_smul, add_mul]
      abel

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 : R
⊢ star x ≤ star y ↔ x ≤ y

Tactic:
suffices ∀ x y, x ≤ y → star x ≤ star y from
    ⟨by simpa only [star_star] using this (star x) (star y), this x y⟩
  intro x y h
  rw [StarOrderedRing.le_iff] at h ⊢
  obtain ⟨d, hd, rfl⟩ := h
  refine ⟨starAddEquiv d, ?_, star_add _ _⟩
  refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd
  rintro - ⟨s, rfl⟩
  exact ⟨s, by simp⟩

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
inst✝ : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 < star x * x

Tactic:
(star_mul_self_nonneg _).lt_iff_ne,

Goal state after:
R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 ≠ star x * x
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ u * x * star u ↔ 0 ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
⊢ 0 ≤ x
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
⊢ LinearIndepOn R f (s ∪ t) ↔ LinearIndepOn R f s ∧ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
  · exact h.mono subset_union_left
  apply (h.mono subset_union_right).map
  simpa [← image_eq_range] using ((linearIndepOn_union_iff hst).1 h).2.2.symm

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✝¹¹ : 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
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = ↑S
x : A
hx : x ∈ s
⊢ star x ∈ (S.copy s hs).carrier

Tactic:
change star x ∈ s

Goal state after:
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
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = ↑S
x : A
hx : x ∈ s
⊢ star x ∈ s
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_2
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 ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥

Tactic:
by_contra H
    rw [not_le, Cardinal.lt_one_iff] at H
    have := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
    have := b.repr.toEquiv.subsingleton
    exact one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p r : R[X]
n : ℕ
⊢ (C ↑n * p).comp r = C ↑n * p.comp r

Tactic:
C_mul_comp

Goal state after:
R : Type u
inst✝ : Semiring R
p r : R[X]
n : ℕ
⊢ C ↑n * p.comp r = C ↑n * p.comp r
Module: Mathlib.Algebra.Polynomial.Eval.Algebra

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
n : ℕ
⊢ eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n

Tactic:
by
  induction n with
  | zero => simp only [pow_zero, eval₂_one]
  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]

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

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

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

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

Goal state before:
pp: case refine_2
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✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : ¬r = 0
w : f (c' • v) = c' • f v
⊢ r • f ((of R M) g • v) + c' • f v = r • (of R M) g • f v + c' • f v

Tactic:
of_apply,

Goal state after:
case refine_2
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✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : ¬r = 0
w : f (c' • v) = c' • f v
⊢ r • f (single g 1 • v) + c' • f v = r • single g 1 • f v + c' • f v
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).leadingCoeff = -p.leadingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).coeff (-p).natDegree = -p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).coeff (-p).natDegree = -p.leadingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).coeff (-p).natDegree = -p.coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.coeff p.natDegree + q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.coeff p.natDegree + q.leadingCoeff = 0

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.coeff p.natDegree + q.coeff q.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
b : ℕ
hp : p.degree ≤ a
⊢ (p ^ b).degree ≤ ↑b * a

Tactic:
induction b with
  | zero => simp [degree_one_le]
  | succ n hn =>
      rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
      exact degree_mul_le_of_le hn hp

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

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

Tactic:
leadingCoeff,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).coeff ((monomial n) a).natDegree = a