harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_apply_of_isMul {x : R} (hx : ∀ y : R, f (x * y) = f x * f y) :
    seminormFromConst' hf1 hc hpm x = f x :=
  have hlim : Tendsto (seminormFromConst_seq c f x) atTop (𝓝 (f x))

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
n : ℕ
hn : n = 0
⊢ seminormFromConst_seq c f x n = f x

Tactic:
simp only [seminormFromConst_seq, hn, pow_zero, mul_one, div_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ seminormFromConst_seq c f x = fun _n => f x

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
n : ℕ
⊢ seminormFromConst_seq c f x n = f x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
hseq : seminormFromConst_seq c f x = fun _n => f x
⊢ Tendsto (fun _n => f x) atTop (𝓝 (f x))

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
n : ℕ
hn : ¬n = 0
⊢ seminormFromConst_seq c f x n = f x

Tactic:
simp only [seminormFromConst_seq, hx (c ^ n), hpm _ (Nat.one_le_iff_ne_zero.mpr hn),
  mul_div_assoc, div_self (pow_ne_zero n hc), mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
hseq : seminormFromConst_seq c f x = fun _n => f x
⊢ Tendsto (seminormFromConst_seq c f x) atTop (𝓝 (f x))

Tactic:
rw [hseq]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
hseq : seminormFromConst_seq c f x = fun _n => f x
⊢ Tendsto (fun _n => f x) atTop (𝓝 (f x))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
n : ℕ
⊢ seminormFromConst_seq c f x n = f x

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
n : ℕ
hn : n = 0
⊢ seminormFromConst_seq c f x n = f x

case neg
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
n : ℕ
hn : ¬n = 0
⊢ seminormFromConst_seq c f x n = f x
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract_of_valid (l m r : List Char) :
    extract ⟨l ++ m ++ r⟩ ⟨utf8Len l⟩ ⟨utf8Len l + utf8Len m⟩ = ⟨m⟩

Proof state:
l m r : List Char
⊢ (if utf8Len l ≥ utf8Len l + utf8Len m then ""
    else { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } }) =
    { data := m }

Tactic:
split

Result:
case isTrue
l m r : List Char
h✝ : utf8Len l ≥ utf8Len l + utf8Len m
⊢ "" = { data := m }

case isFalse
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } } = { data := m }

Proof state:
case isFalse.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₂ (m ++ r) { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m

Tactic:
apply extract.go₂_append_left

Result:
case isFalse.e_data.a
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ utf8Len l + utf8Len m = utf8Len m + utf8Len l

Proof state:
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ utf8Len l = utf8Len l + Pos.byteIdx 0

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m

Tactic:
rw [List.append_assoc, extract.go₁_append_right _ _ _ _ _ (by rfl)]

Result:
case isFalse.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₂ (m ++ r) { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m

Proof state:
l m r : List Char
⊢ { data := l ++ m ++ r }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = { data := m }

Tactic:
simp only [extract]

Result:
l m r : List Char
⊢ (if utf8Len l ≥ utf8Len l + utf8Len m then ""
    else { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } }) =
    { data := m }

Proof state:
case isFalse
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } } = { data := m }

Tactic:
congr

Result:
case isFalse.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m

Proof state:
case isFalse.e_data.a
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ utf8Len l + utf8Len m = utf8Len m + utf8Len l

Tactic:
apply Nat.add_comm

Result:
no goals

Proof state:
case isTrue
l m r : List Char
h✝ : utf8Len l ≥ utf8Len l + utf8Len m
⊢ "" = { data := m }

Tactic:
next h => rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| Nat.add_le_add_iff_left.1 h]

Result:
no goals

Proof state:
l m r : List Char
h : utf8Len l ≥ utf8Len l + utf8Len m
⊢ "" = { data := m }

Tactic:
rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| Nat.add_le_add_iff_left.1 h]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.smul {α E 𝕜 : Type*} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {a b : α → 𝕜} {u v : α → E} {l : Filter α} (hab : a ~[l] b) (huv : u ~[l] v) :
    (fun x ↦ a x • u x) ~[l] fun x ↦ b x • v x

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Tactic:
intro c hc

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Tactic:
refine hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ ?_)

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_eq_iff_eq_mul_left {a b c : Int}
    (H : b ≠ 0) (H' : b ∣ a) : a.tdiv b = c ↔ a = c * b

Proof state:
a b c : Int
H : b ≠ 0
H' : b ∣ a
⊢ a.tdiv b = c ↔ a = b * c

Tactic:
exact Int.tdiv_eq_iff_eq_mul_right H H'

Result:
no goals

Proof state:
a b c : Int
H : b ≠ 0
H' : b ∣ a
⊢ a.tdiv b = c ↔ a = c * b

Tactic:
rw [Int.mul_comm]

Result:
a b c : Int
H : b ≠ 0
H' : b ∣ a
⊢ a.tdiv b = c ↔ a = b * c
-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
/-- The sections of positive strict contractions form a filter basis. -/
lemma isBasis_nonneg_sections :
    IsBasis (fun x : A ↦ 0 ≤ x ∧ ‖x‖ < 1) ({x | · ≤ x}) where
  nonempty := ⟨0, by simp⟩
  inter {x y} hx hy

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
⊢ ∃ k, (0 ≤ k ∧ ‖k‖ < 1) ∧ {x | k ≤ x} ⊆ {x_1 | x ≤ x_1} ∩ {x | y ≤ x}

Tactic:
peel directedOn_nonneg_ball x (by simpa) y (by simpa) with z hz

Result:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
z : A
hz : z ∈ {x | 0 ≤ x} ∩ ball 0 1 ∧ (fun x1 x2 => x1 ≤ x2) x z ∧ (fun x1 x2 => x1 ≤ x2) y z
⊢ (0 ≤ z ∧ ‖z‖ < 1) ∧ {x | z ≤ x} ⊆ {x_1 | x ≤ x_1} ∩ {x | y ≤ x}

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
⊢ x ∈ {x | 0 ≤ x} ∩ ball 0 1

Tactic:
simpa

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
z : A
hz : z ∈ {x | 0 ≤ x} ∩ ball 0 1 ∧ (fun x1 x2 => x1 ≤ x2) x z ∧ (fun x1 x2 => x1 ≤ x2) y z
⊢ 0 ≤ z ∧ ‖z‖ < 1

Tactic:
simpa using hz.1

Result:
no goals

Proof state:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
z : A
hz : z ∈ {x | 0 ≤ x} ∩ ball 0 1 ∧ (fun x1 x2 => x1 ≤ x2) x z ∧ (fun x1 x2 => x1 ≤ x2) y z
⊢ (0 ≤ z ∧ ‖z‖ < 1) ∧ {x | z ≤ x} ⊆ {x_1 | x ≤ x_1} ∩ {x | y ≤ x}

Tactic:
exact ⟨by simpa using hz.1, fun a ha ↦ ⟨hz.2.1.trans ha, hz.2.2.trans ha⟩⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ 0 ≤ 0 ∧ ‖0‖ < 1

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
⊢ y ∈ {x | 0 ≤ x} ∩ ball 0 1

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inr_isoPushout_inv (h : IsPushout f g inl inr) [HasPushout f g] :
    pushout.inr _ _ ≫ h.isoPushout.inv = inr

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ h.isoPushout.inv = inr

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inr
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymm_eq_sum_monomial (n : ℕ) :
    esymm σ R n = ∑ t ∈ powersetCard n univ, monomial (∑ i ∈ t, Finsupp.single i 1) 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymm σ R n = ∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1

Tactic:
simp_rw [monomial_sum_one]

Result:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymm σ R n = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1)) 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymm σ R n = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1)) 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma modByMonic_eq_of_dvd_sub (hq : q.Monic) (h : q ∣ p₁ - p₂) : p₁ %ₘ q = p₂ %ₘ q

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
refine (div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2

Result:
case intro
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁

Tactic:
rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div _ hq, add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
a✝ : Nontrivial R
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
obtain ⟨f, sub_eq⟩ := h

Result:
case intro
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₁ %ₘ q = p₂ %ₘ q

Proof state:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
a✝ : Nontrivial R
⊢ p₁ %ₘ q = p₂ %ₘ q
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem eval₂Hom_eq_constantCoeff_of_vars (f : R →+* S) {g : σ → S} {p : MvPolynomial σ R}
    (hp : ∀ i ∈ p.vars, g i = 0) : eval₂Hom f g p = f (constantCoeff p)

Proof state:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k => g i ^ k) = f (constantCoeff p)

Tactic:
rw [h0, f.map_zero, Finset.sum_eq_zero]

Result:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ ∀ x ∈ p.support, (f (coeff x p) * x.prod fun i k => g i ^ k) = 0

Proof state:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ ∀ x ∈ p.support, (f (coeff x p) * x.prod fun i k => g i ^ k) = 0

Tactic:
intro d hd

Result:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (f (coeff d p) * d.prod fun i k => g i ^ k) = 0

Proof state:
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∈ p.support
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0

Tactic:
intro

Result:
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∈ p.support
a✝ : 0 ∉ p.support
⊢ (f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem map_mul_zero_of_map_zero (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) {x : R} (hx : f x = 0)
    (y : R) : f (x * y) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
y : R
⊢ f (x * y) ≤ 0

Tactic:
simpa [hx] using f_mul x y

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
y : R
⊢ f (x * y) = 0

Tactic:
replace f_mul : f (x * y) ≤ 0 := by simpa [hx] using f_mul x y

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : f x = 0
y : R
f_mul : f (x * y) ≤ 0
⊢ f (x * y) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : f x = 0
y : R
f_mul : f (x * y) ≤ 0
⊢ f (x * y) = 0

Tactic:
exact le_antisymm f_mul (f_nonneg _)

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul {K : Type*} [Field K]
    [IsAlgClosed K] [CharZero K] {f g : K[X]} (hf0 : f ≠ 0) :
    (∀ x, IsRoot f x → IsRoot g x) ↔ f ∣ f.derivative * g

Proof state:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g

Tactic:
intro h

Result:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
h : f.IsRoot a → g.IsRoot a
⊢ rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g

Proof state:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Tactic:
by_cases haf : f.eval a = 0

Result:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : ¬eval a f = 0
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Proof state:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → ∀ (a : K), Multiset.count a f.roots ≤ Multiset.count a (derivative f * g).roots

Tactic:
simp only [count_roots, rootMultiplicity_mul hdg]

Result:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) →
    ∀ (a : K), rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Proof state:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : ¬eval a f = 0
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Tactic:
simp [haf, rootMultiplicity_eq_zero haf]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ‖(n : ℂ)‖ = n

Proof state:
n : ℤ
hn : 0 ≤ n
⊢ ‖↑n‖ = ↑n

Tactic:
rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_copy (hu : u = u') (hv : v = v') :
    (p.copy hu hv).map f = (p.map f).copy (hu ▸ rfl) (hv ▸ rfl)

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ Walk.map f (p.copy hu hv) = (Walk.map f p).copy ⋯ ⋯

Tactic:
subst_vars

Result:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u' v' : V
p : G.Walk u' v'
⊢ Walk.map f (p.copy ⋯ ⋯) = (Walk.map f p).copy ⋯ ⋯

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u' v' : V
p : G.Walk u' v'
⊢ Walk.map f (p.copy ⋯ ⋯) = (Walk.map f p).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem norm_add_le' (z w : ℂ) :  ‖z + w‖ ≤ ‖z‖ + ‖w‖ :=
  (mul_self_le_mul_self_iff (norm_nonneg (z + w)) (add_nonneg (norm_nonneg z)
    (norm_nonneg w))).2 <| by
    rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
      add_right_comm, normSq_add, add_le_add_iff_left, mul_assoc, mul_le_mul_left (zero_lt_two' ℝ),
      norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z, ← normSq_conj w, ← map_mul]
    exact re_le_norm (z * conj w)

Proof state:
z w : ℂ
⊢ (z * (starRingEnd ℂ) w).re ≤ √(normSq (z * (starRingEnd ℂ) w))

Tactic:
exact re_le_norm (z * conj w)

Result:
no goals

Proof state:
z w : ℂ
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)

Tactic:
rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
  add_right_comm, normSq_add, add_le_add_iff_left, mul_assoc, mul_le_mul_left (zero_lt_two' ℝ),
  norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z, ← normSq_conj w, ← map_mul]

Result:
z w : ℂ
⊢ (z * (starRingEnd ℂ) w).re ≤ √(normSq (z * (starRingEnd ℂ) w))
-- Mathlib/RingTheory/LocalRing/Module.lean
theorem map_tensorProduct_mk_eq_top {N : Submodule R M} [Module.Finite R M] :
    N.map (TensorProduct.mk R k M 1) = ⊤ ↔ N = ⊤

Proof state:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((mk R k M) 1) N = ⊤
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
hf : Surjective ⇑f
⊢ N = ⊤

Tactic:
apply_fun Submodule.map f at hN

Result:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
this✝¹ : Module k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
this✝ : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • ⊤))
f : k ⊗[R] M →ₗ[R] M ⧸ 𝔪 • ⊤ :=
  AlgebraTensorModule.lift (↑R ((LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ 𝔪 • ⊤)).symm (𝔪 • ⊤).mkQ))
this : f ∘ₗ (mk R k M) 1 = (𝔪 • ⊤).mkQ
hf : Surjective ⇑f
hN : Submodule.map f (Submodule.map ((mk R k M) 1) N) = Submodule.map f ⊤
⊢ N = ⊤