mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)

Tactic:
simp only [isSelfAdjoint_iff, star_sub, hx.star_eq, hy.star_eq]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝¹ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
x : M
x✝ : x ∈ ⊤
⊢ x ∈ span R (Set.range (Fin.cons y (⇑N.subtype ∘ ⇑b)))

Tactic:
by simpa [Submodule.mem_span_insert', span_b] using hsp x

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂

Tactic:
h₁₁,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ fromBlocks B.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝¹ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
x : M
x✝ : x ∈ ⊤
⊢ x ∈ span R (Set.range (Fin.snoc (⇑N.subtype ∘ ⇑b) y))

Tactic:
by simpa [Submodule.mem_span_insert', span_b] using hsp x

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i ↦ ¬q i) * B.toBlock (fun i ↦ ¬q i) r

Tactic:
ext i k
  simp only [toBlock_apply, mul_apply]
  exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
| I ≤ Ideal.span {x}

Tactic:
rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
| generator I ∈ Ideal.span {x}
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q).symm (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q)) = (a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)

Tactic:
by
  apply ((distribBaseChange R A N Q).eq_symm_apply.mpr ?_).symm
  rw [tmul_eq_smul_one_tmul b, ← smul_tmul, smul_tmul', mul_comm]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
N : Type uN
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ cancelBaseChange R A A A N = TensorProduct.lid A (A ⊗[R] N)

Tactic:
by
  ext x
  induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul b y =>
    induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
  | add x y hx hy => simp [hx, hy]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: 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 : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ False

Tactic:
replace hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s := by
    rw [← hm, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]

Goal state after:
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 → ℕ
hn : ∏ a ∈ S, a ^ n a = b
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
⊢ False
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
⊢ Submodule.map M.vecMulLinear ⊤ = span R (Set.range M.row)

Tactic:
← iSup_range_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
⊢ Submodule.map M.vecMulLinear (⨆ i, (LinearMap.single R (fun i ↦ R) i).range) = span R (Set.range M.row)
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsFractionRing R R ↔ R⁰ ≤ IsUnit.submonoid R

Tactic:
self_iff_nonZeroDivisors_eq_isUnit,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ R⁰ = IsUnit.submonoid R ↔ R⁰ ≤ IsUnit.submonoid R
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
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun
      ((algebraMap B FB) ((algebraMap A B) x) / (algebraMap B FB) ((algebraMap A B) y)) =
    (algebraMap A FC) x / (algebraMap A FC) y

Tactic:
simp [← IsScalarTower.algebraMap_apply A C FC]

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 a b - mk c d = mk (↑d * a - ↑b * c) (b * d)

Tactic:
rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
f : A ⊗[R] A →ₗ[R] A ⊗[R] M :=
  lift
    { toFun := fun x ↦ { toFun := fun y ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
⊢ 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m

Tactic:
simpa [f] using! congr_arg f (tmul_comm R 1 a)

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ quasispectrum R a = spectrum R ↑a

Tactic:
ext r
  have := Set.singleton_subset_iff.mpr (zero_mem_spectrum_inr R S a)
  rw [← Set.union_eq_self_of_subset_right this, ← quasispectrum_eq_spectrum_union_zero]
  apply forall_congr' fun x ↦ ?_
  rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (m x : A), (m • x) • baseChangeHom R A M N = (RingHom.id A) m • x • baseChangeHom R A M N

Tactic:
simp only [smul_assoc, RingHom.id_apply, forall_true_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
⊢ False

Tactic:
rw [eq, rank_bot] at h

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < 0
eq : s = ⊥
⊢ False
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Goal state after:
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
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 = 0 w
⊢ ∃ w, f w = 1

Tactic:
use (f w)⁻¹ • w

Goal state after:
case h
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := ⋯
w : V
hw : ¬f w = 0 w
⊢ f ((f w)⁻¹ • w) = 1
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
⊢ IsMulCommutative ↥(adjoin R s)

Tactic:
have := adjoin_le_centralizer_centralizer R s
  refine .of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_
  have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
    Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
      (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
  apply this at h₁
  apply this at h₂
  rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
  exact Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)

Tactic:
simpa [bS] using bS.linearIndependent.linearIndepOn_id.image
      (f := Submodule.subtype S) (by simp)

Goal state after:
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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ⇑(f.domRestrict p) ↔ Surjective ⇑(f.restrict h)

Tactic:
simp [disjoint_iff, ← injective_iff_surjective]

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
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : ↑(r • ⟨v₀, hv₀⟩) = ↑⟨v, hv⟩
⊢ r • v₀ = v

Tactic:
coe_smul

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
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ↑⟨v₀, hv₀⟩ = ↑⟨v, hv⟩
⊢ r • v₀ = v
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
x✝¹ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
x✝ : ↥s
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ ↑(r • ⟨v₀, hv₀⟩) = ↑⟨v, hv⟩

Tactic:
coe_smul

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
x✝¹ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
x✝ : ↥s
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • ↑⟨v₀, hv₀⟩ = ↑⟨v, hv⟩
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 u_1
inst✝ : Unique ι
⊢ Nonempty (Basis ι K V) → finrank K V = 1

Tactic:
rintro ⟨b⟩

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 u_1
inst✝ : Unique ι
b : Basis ι K V
⊢ finrank 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
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))

Tactic:
pow_add f k m,

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False

Tactic:
by
    classical exact fun hxy : x ≠ y ↦
        let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
        have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
        have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
        have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
        one_ne_zero <| hfy1.symm.trans hfy0

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

Goal state before:
pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0

Tactic:
· exact False.elim (CharP.char_ne_one R 1 rfl)

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

Goal state before:
pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R

Tactic:
· exact False.elim (CharP.char_ne_one R 1 rfl)

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 (Icc a b)
h₁ : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ico a c) b

Tactic:
intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀
  · exact 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
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✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝¹ x✝ : AddAut M
⊢ Additive.ofMul (domCongr R A (x✝¹ + x✝)) = Additive.ofMul (domCongr R A x✝¹) + Additive.ofMul (domCongr R A x✝)

Tactic:
ext; simp [AddAut.add_def]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ WithBot.unbotD 0 (C a).degree = 0

Tactic:
degree_C ha,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ WithBot.unbotD 0 0 = 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * φ.coeff c

Tactic:
apply dvd_mul_right

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

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

Tactic:
simp [natDegree]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff ≠ 0 ↔ p ≠ 0

Tactic:
by rw [Ne, leadingCoeff_eq_zero]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)

Tactic:
have := supp_subset_range hn

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
this : p.support ⊆ range n
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f

Tactic:
by
  by_cases hp : p = 0
  · rw [hp, sum_zero_index, Finset.sum_eq_zero]
    intro i _
    exact hf i
  rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
    Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ p.leadingCoeff = 1

Tactic:
nontriviality

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
· rw [hp2, zero_mul, coeff_zero]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = 1

Tactic:
rw [← coeff_one_zero, ← hgf]
    simp

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

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

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ ((X + C r) ^ i).leadingCoeff = 1

Tactic:
nontriviality

Goal state after:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ ((X + C r) ^ i).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 ↔ ∃ n a, f = (monomial n) a

Tactic:
by
  constructor
  · intro H
    rw [Finset.card_le_one_iff_subset_singleton] at H
    rcases H with ⟨n, hn⟩
    refine ⟨n, f.coeff n, ?_⟩
    ext i
    by_cases hi : i = n
    · simp [hi]
    · have : f.coeff i = 0 := by
        rw [← notMem_support_iff]
        exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
      simp [this, Ne.symm hi, coeff_monomial]
  · rintro ⟨n, a, rfl⟩
    rw [← Finset.card_singleton n]
    apply Finset.card_le_card
    exact support_monomial_subset _ _

Goal state after: