mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
x : B
hr : (algebraMap A B) r ∈ B'
hx : ∃ l, (Finsupp.linearCombination R Subtype.val) l = x
⊢ ∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ B'

Tactic:
rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
⊢ ∃ n₀, ∀ n ≥ n₀, (r ^ n • l.sum fun i c ↦ c • ↑i) ∈ B'
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : NonUnitalSubalgebra R A
⊢ span R ↑(Submonoid.closure ↑s) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
Submonoid.closure_eq_one_union,

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : NonUnitalSubalgebra R A
⊢ span R ({1} ∪ ↑(Subsemigroup.closure ↑s)) = R ∙ 1 ⊔ s.toSubmodule
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Injective ⇑(ringEquivOfRingEquivHom A K)

Tactic:
intro f

Goal state after:
A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f : A ≃+* A
⊢ ∀ ⦃a₂ : A ≃+* A⦄, (ringEquivOfRingEquivHom A K) f = (ringEquivOfRingEquivHom A K) a₂ → f = a₂
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
⊢ Injective ⇑(fieldEquivOfAlgEquivHom K L)

Tactic:
intro f

Goal state after:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f : B ≃ₐ[A] B
⊢ ∀ ⦃a₂ : B ≃ₐ[A] B⦄, (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) a₂ → f = a₂
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inl
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Nontrivial R
right✝ : Subsingleton S
⊢ False

pp: case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ False

Tactic:
· obtain ⟨c, hc⟩ := h.exists_of_eq (x := 1) (y := 0) (Subsingleton.elim _ _)
    simp at hc

Goal state after:
case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ False
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ image2 (fun a b ↦ (a * b)⋆) s t = image2 (fun a b ↦ a⋆ * b⋆) t s

Tactic:
star_mul,

Goal state after:
α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ image2 (fun a b ↦ b⋆ * a⋆) s t = image2 (fun a b ↦ a⋆ * b⋆) t s
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommSemiring α

Tactic:
apply e.injective.commSemiring _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: case tmul
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
⊢ r • (x * a ⊗ₜ[R] b) = x * r • a ⊗ₜ[R] b

Tactic:
induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
      | add x y hx hy => simp [smul_add, add_mul _, *]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - a)

Tactic:
simpa only [smul_inv_smul] using IsUnit.smul r hu

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
inst✝ : Nontrivial A
⊢ σ 0 = {0}

Tactic:
by
  refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
  rw [spectrum, Set.compl_subset_comm]
  intro k hk
  rw [Set.mem_compl_singleton_iff] at hk
  have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
  simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a₁ a₂ b₁ b₂ : S
⊢ (let __spread.0 := LinearMap.mul' R S;
      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
      ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    (let __spread.0 := LinearMap.mul' R S;
        { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
        (a₁ ⊗ₜ[R] b₁) *
      (let __spread.0 := LinearMap.mul' R S;
        { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
        (a₂ ⊗ₜ[R] b₂)

Tactic:
by simp [mul_mul_mul_comm]

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
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
⊢ star c * (fun s ↦ star s * s) x * c = star (x * c) * (x * c)

Tactic:
star_mul,

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
⊢ star c * (fun s ↦ star s * s) x * c = star c * star x * (x * c)
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mpr.add
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 A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (y + z) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (y + z) * includeLeft x

Tactic:
| add y z hy hz =>

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:
rw [(star_mul_self_nonneg _).lt_iff_ne, ← mul_zero (star x), hx.star.left.ne_iff]
  exact hx.ne_zero.symm

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v ∈ V ↑i, v ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
choose v hvV hv using hI

Goal state after:
ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
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✝³ : StrongRankCondition R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ 0 < finrank R M ↔ ∃ x, x ≠ 0

Tactic:
by
  rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank]
  norm_cast

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 : V
hfv : f v = 0
hf : f ≠ 0
hv : v ≠ 0
⊢ ∃ n b i j, i ≠ j ∧ v = b i ∧ f = b.coord j

Tactic:
lift v to ker f using hfv
  have : LinearIndepOn K _root_.id {v} := by simpa using hv
  set b₁ : Basis _ K (ker f) := .extend this
  obtain ⟨w, hw⟩ : ∃ w, f w = 1 := by
    simp only [ne_eq, DFunLike.ext_iff, not_forall] at hf
    rcases hf with ⟨w, hw⟩
    use (f w)⁻¹ • w
    simp_all
  set s : Set V := (ker f).subtype '' Set.range b₁
  have hs : span K s = ker f := by
    simp only [s, span_image]
    simp
  have hvs : ↑v ∈ s := by
    refine ⟨v, ?_, by simp⟩
    simp [b₁, this.subset_extend _ _]
  set n := insert w s
  have H₁ : LinearIndepOn K _root_.id n := by
    apply LinearIndepOn.id_insert
    · apply LinearIndepOn.image
      · exact b₁.linearIndependent.linearIndepOn_id
      · simp
    · simp [hs, hw]
  have H₂ : ⊤ ≤ span K n := by
    rintro x -
    simp only [n, mem_span_insert']
    use -f x
    simp [hs, hw]
  set b := Basis.mk H₁ (by simpa using H₂)
  refine ⟨n, b, ⟨v, by simp [n, hvs]⟩, ⟨w, by simp [n]⟩, ?_, by simp [b], ?_⟩
  · apply_fun (f ∘ (↑))
    simp [hw]
  · apply b.ext
    intro i
    rw [Basis.coord_apply, Basis.repr_self]
    simp only [b]
    rcases i with ⟨x, rfl | ⟨x, hx, rfl⟩⟩
    · simp [hw]
    · suffices x ≠ w by simp [this]
      apply_fun f
      simp [hw]

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
⊢ ∀ (a b c : E →ₛₗ.[σ] F), a ≤ b → a ≤ c → a ≤ { domain := b.eqLocus c, toFun := b.toFun ∘ₛₗ inclusion ⋯ }

Tactic:
intro f

Goal state after:
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 : E →ₛₗ.[σ] F
⊢ ∀ (b c : E →ₛₗ.[σ] F), f ≤ b → f ≤ c → f ≤ { domain := b.eqLocus c, toFun := b.toFun ∘ₛₗ inclusion ⋯ }
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
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ #V < ℵ₀

Tactic:
← lift_lt_aleph0.{v, u},

Goal state after:
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{u, v} #V < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K✝ : Type u
V : Type v
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ (x * if H : x = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
rw [dif_neg hx]

Goal state after:
K✝ : Type u
V : Type v
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ x * Classical.choose ⋯ = 1
Module: Mathlib.Algebra.FreeAlgebra

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

Tactic:
← smul_assoc

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) {a} x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support

Tactic:
rw [image₂_singleton_left]

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

Goal state before:
pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ n.minFacProp (if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
by_cases dk : k ∣ n

Goal state after:
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp (if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3

Tactic:
simp [k, e, Nat.left_distrib, add_right_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
k : ℕ
this : ∀ (a : ℕ), ↑(p * a) = 0
⊢ ↑k = ↑(k % p + p * (k / p))

Tactic:
rw [Nat.mod_add_div]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
⊢ (z • f).graph = Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

Tactic:
ext ⟨x_fst, x_snd⟩

Goal state after:
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ (z • f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ n.minFacProp n.minFac

Tactic:
simp [n0, minFacProp]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ (-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
ext ⟨x_fst, x_snd⟩

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ (-f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ m.Coprime n

Tactic:
by
  rw [coprime_iff_gcd_eq_one]
  by_contra g2
  obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
  apply H p hp <;> apply dvd_trans hpdvd
  · exact gcd_dvd_left _ _
  · exact gcd_dvd_right _ _

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ y₁ = y₂

Tactic:
have hy : ((0 : E), y₁ - y₂) ∈ g := by
    convert! g.sub_mem hy₁ hy₂
    exact (sub_self _).symm

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ y₁ = y₂
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
⊢ g.toLinearPMap.graph = g

Tactic:
ext ⟨x_fst, x_snd⟩

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g
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.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p.toFinsupp * q.toFinsupp).coeff.support ≤ #(p.toFinsupp.coeff.support + q.toFinsupp.coeff.support)

Tactic:
grw [AddMonoidAlgebra.support_coeff_mul_subset]

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

Goal state before:
pp: R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ∑ n ∈ p.support, (f n) ((c • p).coeff n) = (RingHom.id R) c • p.sum fun x1 x2 ↦ (f x1) x2

Tactic:
simp only [sum_def, Finset.smul_sum, coeff_smul, map_smul, RingHom.id_apply]

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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb

Tactic:
by
  rw [← List.prod_replicate, ← List.sum_replicate]
  refine (sup_support_list_prod_le degb0 degbm _).trans_eq ?_
  rw [List.map_replicate]

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

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

Tactic:
ext (_ | n)
  · simp
  rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]
  exact h.trans_lt (WithBot.coe_lt_coe.2 n.succ_pos)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
lhs

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (p - q).degree
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥

pp: case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
· exact (not_lt_bot h).elim

Goal state after:
case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
h : ↑a✝ < ⊥
⊢ ↑a✝ + 1 ≤ ⊥

pp: case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Tactic:
· exact (not_lt_bot h).elim

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
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 ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
⊢ ∑ i ∈ s, f i ≠ 0

pp: case neg
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 ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∃ k ∈ s, k ≠ i
⊢ ∑ i ∈ s, f i ≠ 0

Tactic:
· refine (sum_eq_single_of_mem j hj (fun k hk hne => ?_)).trans_ne hne
    rw [h k hk, h j hj] at hne; exact hne.irrefl.elim

Goal state after:
case neg
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 ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∃ k ∈ s, k ≠ i
⊢ ∑ i ∈ s, f i ≠ 0