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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • x + ⅟2 • x = x

Tactic:
invOf_two_smul_add_invOf_two_smul

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ x = x
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (diagonal v).toBlocks₁₁ = diagonal fun i ↦ v (Sum.inl i)

Tactic:
by
  unfold toBlocks₁₁
  funext i j
  simp only [Sum.inl.injEq, of_apply, diagonal_apply]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ (A.submatrix ⇑e ⇑f).updateRow i r i' j = (A.updateRow (e i) fun j ↦ r (f.symm j)).submatrix (⇑e) (⇑f) i' j

Tactic:
simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
j : m
r : α
B : Matrix m n α
⊢ single i j r * B = updateRow 0 i (r • B.row j)

Tactic:
rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩

Tactic:
obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
        mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂' : R
hr₂' : r₂' ∈ R ∙ ψ ⟨y, ⋯⟩
hr₁ : generator (span R {a, ψ ⟨y, ⋯⟩}) = r₁ • a + r₂'
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ r₁ * ϕ ⟨y, ⋯⟩ + r₂ * ψ ⟨y, ⋯⟩ = d

Tactic:
d_eq,

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ r₁ * ϕ ⟨y, ⋯⟩ + r₂ * ψ ⟨y, ⋯⟩ = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
⊢ False

Tactic:
obtain h | h : m r = 0 ∨ n r = 0 := by lia

Goal state after:
case inl
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : m r = 0
⊢ False

case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
⊢ False
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ 0 * x = 0

Tactic:
induction x using OreLocalization.ind with | _ r s
    rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_1.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
z : O
zN : z ∈ N
b : R
hb : ϕ ⟨z, ⋯⟩ = generator (ϕ.submoduleImage N) * b
⊢ ϕ (⟨z, ⋯⟩ - b • ⟨y, ⋯⟩) = 0

Tactic:
rw [map_sub, map_smul, hb, ϕy_eq, smul_eq_mul, mul_comm, sub_self]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n

Tactic:
choose n o hno bO bN a snf using N.exists_smith_normal_form_of_le b O N_le_O

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
n o : ℕ
hno : n ≤ o
bO : Basis (Fin o) R ↥O
bN : Basis (Fin n) R ↥N
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x : Localization S
⊢ ∃ a, (mapPiEvalRingHom S) a = x

Tactic:
· obtain ⟨r, s, rfl⟩ := exists_mk'_eq S x
    exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
      by simp [map_mk']⟩

Goal state after:
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
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ f.comp (algebraMap R S) = (↑(algEquiv M S Q)).comp (algebraMap R S)

Tactic:
rw [hf]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ algebraMap R Q = (↑(algEquiv M S Q)).comp (algebraMap R S)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submonoid R
hM : Algebra.algebraMapSubmonoid S M ≤ IsUnit.submonoid S
h : Bijective ⇑(algebraMap R S)
x y : R
hxy : (algebraMap R S) x = (algebraMap R S) y
⊢ ↑1 * x = ↑1 * y

Tactic:
by simp [h.injective hxy]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
⊢ Module.Finite A (TensorProduct R A M)

Tactic:
by
  classical
    obtain ⟨s, hs⟩ := h.fg_top
    refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
    rintro x -
    induction x with
    | zero => exact zero_mem _
    | tmul x y =>
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs,
        Submodule.map_top, LinearMap.coe_range, ← mul_one x, ← smul_eq_mul,
        ← TensorProduct.smul_tmul']
      exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)
    | add x y hx hy => exact Submodule.add_mem _ hx hy

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y

Tactic:
use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp

Goal state after:
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) ((LinearMap.liftBaseChange S ↑f) x)) ((LinearMap.liftBaseChange S ↑f) y)

Tactic:
← LinearMap.compl₁₂_apply

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)) x) y =
    (((LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)) x) y
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} #m * lift.{u, v} #n

Tactic:
lift_umax.{v, u}

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{u, v} #m * lift.{u, v} #n = lift.{u, v} #m * lift.{u, v} #n
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
⊢ Basis (m ⊕ n) R V

Tactic:
let b : m ⊕ n → V := Sum.elim (fun i ↦ bW i) ((Function.surjInv W.mkQ_surjective) ∘ bQ)

Goal state after:
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
⊢ Basis (m ⊕ n) R V
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case left
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ∃ x ∈ K ∙ v, x ≠ 0

Tactic:
exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩

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

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
s : Set V
si : LinearIndepOn K id s
⊢ #↑s ≤ Module.rank K V

Tactic:
exact si.cardinal_le_rank

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀

Tactic:
rank_le_one_iff,

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀
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
⊢ finrank K ↥(K ∙ v) ≤ 1

pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K ↥(K ∙ v)

Tactic:
· exact finrank_span_le_card ({v} : Set V)

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
⊢ 1 ≤ finrank K ↥(K ∙ v)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

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

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq, mul_add]
  | monomial n b => simp [mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R

Tactic:
rw [ringChar.eq_iff, charP_zero_iff_charZero]

Goal state after:
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
    rw [ringExpChar, ringChar.eq R 0]; rfl

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

Goal state before:
pp: case neg
α : 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)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
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: R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Monoid M
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : M →* A
x : R[M]
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) x) = ((lift R A M) f) x

Tactic:
by
  induction x using induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]

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

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₀ ⟨hx, g₀⟩ (right_mem_Icc.2 (hx.trans g₀)) g₀

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddMonoid M
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : Multiplicative M →* A
x : R[M]
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) x) = ((lift R A M) f) x

Tactic:
by
  induction x using induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]

Goal state after:
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]
hp : p ≠ 0
hpq : p.degree < q.degree
⊢ p.natDegree < q.natDegree

Tactic:
by_cases hq : q = 0
  · exact (not_lt_bot <| hq ▸ hpq).elim
  rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq

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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ leadingCoeff D (q + p) = leadingCoeff D q

Tactic:
leadingCoeff_add_eq_left h

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ leadingCoeff D q = leadingCoeff D q
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ∈ s.erase i
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
Finset.mem_erase

Goal state after:
case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ p.natDegree = 0

Tactic:
by rw [h, natDegree_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).natDegree ≤ n

Tactic:
by
  nontriviality R
  rw [Polynomial.natDegree_X_pow]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))

Tactic:
simp [eval₂_finsetSum, eval₂_pow]

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y

Tactic:
· rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'

Tactic:
by simpa using congr($h X)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range n, (algebraMap R S) (p.coeff x_1) * x ^ x_1

Tactic:
exact eval₂_eq_sum_range' (algebraMap R S) hn x

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (Finsupp.single n e + s)) a = X n ^ e * (monomial s) a

Tactic:
by
  rw [X_pow_eq_monomial, monomial_mul, one_mul]

Goal state after: