harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem ofReal_norm_sub_eq_lintegral (f g : α →₁[μ] β) :
    ENNReal.ofReal ‖f - g‖ = ∫⁻ x, ‖f x - g x‖ₑ ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ

Tactic:
apply lintegral_congr_ae

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (fun a => edist (↑↑(f - g) a) 0) =ᶠ[ae μ] fun a => edist (↑↑f a - ↑↑g a) 0

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0

Tactic:
simp only [ha, Pi.sub_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ

Tactic:
simp_rw [ofReal_norm_eq_lintegral, ← edist_zero_eq_enorm]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (fun a => edist (↑↑(f - g) a) 0) =ᶠ[ae μ] fun a => edist (↑↑f a - ↑↑g a) 0

Tactic:
filter_upwards [Lp.coeFn_sub f g] with _ ha

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0
-- Mathlib/Data/Int/Init.lean
lemma toNat_le_toNat {a b : ℤ} (h : a ≤ b) : toNat a ≤ toNat b

Proof state:
a b : ℤ
h : a ≤ b
⊢ a ≤ ↑b.toNat

Tactic:
exact Int.le_trans h (self_le_toNat b)

Result:
no goals

Proof state:
a b : ℤ
h : a ≤ b
⊢ a.toNat ≤ b.toNat

Tactic:
rw [toNat_le]

Result:
a b : ℤ
h : a ≤ b
⊢ a ≤ ↑b.toNat
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
lemma Even.gammaFactor_def {χ : DirichletCharacter ℂ N} (hχ : χ.Even) (s : ℂ) :
    gammaFactor χ s = Gammaℝ s

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Even
s : ℂ
⊢ χ.gammaFactor s = s.Gammaℝ

Tactic:
simp [gammaFactor, hχ]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
@[to_additive]
lemma mem_pow_iff_prod {n : ℕ} {s : Set α} {a : α} :
    a ∈ s ^ n ↔ ∃ f : Fin n → α, (∀ i, f i ∈ s) ∧ ∏ i, f i = a

Proof state:
α : Type u_2
inst✝ : CommMonoid α
n : ℕ
s : Set α
a : α
⊢ a ∈ s ^ n ↔ ∃ f, (∀ (i : Fin n), f i ∈ s) ∧ ∏ i : Fin n, f i = a

Tactic:
simpa using mem_finset_prod (t := .univ) (f := fun _ : Fin n ↦ s) _

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem moveLeft_nim_hEq (o : Ordinal) :
    HEq (nim o).moveLeft fun i : o.toType => nim ((enumIsoToType o).symm i)

Proof state:
o : Ordinal.{u_1}
⊢ HEq (nim o).moveLeft fun i => nim ↑(o.enumIsoToType.symm i)

Tactic:
rw [nim]

Result:
o : Ordinal.{u_1}
⊢ HEq (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).moveLeft
    fun i => nim ↑(o.enumIsoToType.symm i)

Proof state:
o : Ordinal.{u_1}
⊢ HEq (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).moveLeft
    fun i => nim ↑(o.enumIsoToType.symm i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem flip_isReduced : (flip u).IsReduced ↔ u.IsReduced

Proof state:
u : XgcdType
⊢ u.flip.IsReduced ↔ u.IsReduced

Tactic:
dsimp [IsReduced, flip]

Result:
u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp

Proof state:
u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp

Tactic:
constructor <;> intro h <;> exact h.symm

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive sum_le_sum]
lemma Forall₂.prod_le_prod' [Preorder M] [MulRightMono M]
    [MulLeftMono M] {l₁ l₂ : List M} (h : Forall₂ (· ≤ ·) l₁ l₂) :
    l₁.prod ≤ l₂.prod

Proof state:
case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
a b : M
la lb : List M
hab : a ≤ b
ih : Forall₂ (fun x1 x2 => x1 ≤ x2) la lb
ih' : la.prod ≤ lb.prod
⊢ (a :: la).prod ≤ (b :: lb).prod

Tactic:
simpa only [prod_cons] using mul_le_mul' hab ih'

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction' h with a b la lb hab ih ih'

Result:
case nil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
⊢ [].prod ≤ [].prod

case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
a b : M
la lb : List M
hab : a ≤ b
ih : Forall₂ (fun x1 x2 => x1 ≤ x2) la lb
ih' : la.prod ≤ lb.prod
⊢ (a :: la).prod ≤ (b :: lb).prod

Proof state:
case nil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
⊢ [].prod ≤ [].prod

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma sup_edge_of_adj (h : G.Adj s t) : G ⊔ edge s t = G

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
⊢ G ⊔ edge s t = G

Tactic:
rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edge_edgeSet_of_ne h.ne, Set.singleton_subset_iff,
  mem_edgeSet]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem prod_coe_rpow {ι} (s : Finset ι) (f : ι → ℝ≥0) (r : ℝ) :
    ∏ i ∈ s, (f i : ℝ≥0∞) ^ r = ((∏ i ∈ s, f i : ℝ≥0) : ℝ≥0∞) ^ r

Proof state:
case empty
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ ∅, ↑(f i) ^ r = ↑(∏ i ∈ ∅, f i) ^ r

Tactic:
simp

Result:
no goals

Proof state:
case insert
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
ih : ∏ i ∈ s✝, ↑(f i) ^ r = ↑(∏ i ∈ s✝, f i) ^ r
⊢ ∏ i ∈ insert a✝ s✝, ↑(f i) ^ r = ↑(∏ i ∈ insert a✝ s✝, f i) ^ r

Tactic:
simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with
| empty => simp
| insert hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r

Tactic:
classical
induction s using Finset.induction with
| empty => simp
| insert hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem zipIdx_append (xs ys : List α) (k : Nat) :
    zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.length)

Proof state:
case cons
α : Type u_1
x : α
xs : List α
IH : ∀ (ys : List α) (k : Nat), (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.length)
ys : List α
k : Nat
⊢ (x :: xs ++ ys).zipIdx k = (x :: xs).zipIdx k ++ ys.zipIdx (k + (x :: xs).length)

Tactic:
rw [cons_append, zipIdx_cons, IH, ← cons_append, ← zipIdx_cons, length, Nat.add_right_comm,
  Nat.add_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
ys : List α
k : Nat
⊢ ([] ++ ys).zipIdx k = [].zipIdx k ++ ys.zipIdx (k + [].length)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs ys : List α
k : Nat
⊢ (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.length)

Tactic:
induction xs generalizing ys k with
| nil => simp
| cons x xs IH =>
  rw [cons_append, zipIdx_cons, IH, ← cons_append, ← zipIdx_cons, length, Nat.add_right_comm,
    Nat.add_assoc]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contDiffWithinAtProp_self_source {f : E → H'} {s : Set E} {x : E} :
    ContDiffWithinAtProp 𝓘(𝕜, E) I' n f s x ↔ ContDiffWithinAt 𝕜 n (I' ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : WithTop ℕ∞
f : E → H'
s : Set E
x : E
⊢ ContDiffWithinAtProp 𝓘(𝕜, E) I' n f s x ↔ ContDiffWithinAt 𝕜 n (↑I' ∘ f) s x

Tactic:
simp_rw [ContDiffWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
  modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem localTriv_continuousLinearMapAt {b : B} (hb : b ∈ Z.baseSet i) :
    (Z.localTriv i).continuousLinearMapAt R b = Z.coordChange (Z.indexAt b) i b

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
⊢ Trivialization.continuousLinearMapAt R (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b

Tactic:
ext1 v

Result:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : Z.Fiber b
⊢ (Trivialization.continuousLinearMapAt R (Z.localTriv i) b) v = (Z.coordChange (Z.indexAt b) i b) v

Proof state:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : Z.Fiber b
⊢ (Trivialization.continuousLinearMapAt R (Z.localTriv i) b) v = (Z.coordChange (Z.indexAt b) i b) v

Tactic:
rw [(Z.localTriv i).continuousLinearMapAt_apply R, (Z.localTriv i).coe_linearMapAt_of_mem]

Result:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : Z.Fiber b
⊢ (fun y => (↑(Z.localTriv i) { proj := b, snd := y }).2) v = (Z.coordChange (Z.indexAt b) i b) v

case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : Z.Fiber b
⊢ b ∈ (Z.localTriv i).baseSet

Proof state:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : Z.Fiber b
⊢ (fun y => (↑(Z.localTriv i) { proj := b, snd := y }).2) v = (Z.coordChange (Z.indexAt b) i b) v

case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : Z.Fiber b
⊢ b ∈ (Z.localTriv i).baseSet

Tactic:
exacts [rfl, hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : List α} {k : Nat} :
    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1

Proof state:
α : Type u_1
x : α × Nat
l : List α
k : Nat
⊢ x ∈ l.zipIdx k ↔ k ≤ x.snd ∧ l[x.snd - k]? = some x.fst

Tactic:
cases x

Result:
case mk
α : Type u_1
l : List α
k : Nat
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx k ↔ k ≤ (fst✝, snd✝).snd ∧ l[(fst✝, snd✝).snd - k]? = some (fst✝, snd✝).fst

Proof state:
case mk
α : Type u_1
l : List α
k : Nat
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx k ↔ k ≤ (fst✝, snd✝).snd ∧ l[(fst✝, snd✝).snd - k]? = some (fst✝, snd✝).fst

Tactic:
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_closure_range_iff_nat {e : β → α} {a : α} :
    a ∈ closure (range e) ↔ ∀ n : ℕ, ∃ k : β, dist a (e k) < 1 / ((n : ℝ) + 1) :=
  (mem_closure_iff_nhds_basis nhds_basis_ball_inv_nat_succ).trans <| by
    simp only [mem_ball, dist_comm, exists_range_iff, forall_const]

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
e : β → α
a : α
⊢ (∀ (i : ℕ), True → ∃ y ∈ range e, y ∈ ball a (1 / (↑i + 1))) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)

Tactic:
simp only [mem_ball, dist_comm, exists_range_iff, forall_const]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_smul_choose [NatPowAssoc R] (r : R) {n k : ℕ} (hkn : k ≤ n) :
    (Nat.choose n k) • choose r n = choose r k * choose (r - k) (n - k)

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ (n - k + k)).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Tactic:
rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
  ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • choose r n = choose r k * choose (r - ↑k) (n - k)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero n),
  nsmul_left_comm, ← descPochhammer_eq_factorial_smul_choose,
  ← Nat.choose_mul_factorial_mul_factorial hkn, ← smul_mul_smul_comm,
  ← descPochhammer_eq_factorial_smul_choose, mul_nsmul',
  ← descPochhammer_eq_factorial_smul_choose, smul_mul_assoc]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ n).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ n).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Tactic:
nth_rw 2 [← Nat.sub_add_cancel hkn]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ (n - k + k)).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem trailingDegree_mul : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(p.natTrailingDegree + q.natTrailingDegree) = ↑p.natTrailingDegree + ↑q.natTrailingDegree

Tactic:
apply WithTop.coe_add

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [hp, zero_mul, trailingDegree_zero, top_add]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [hq, mul_zero, trailingDegree_zero, add_top]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]

Result:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(p.natTrailingDegree + q.natTrailingDegree) = ↑p.natTrailingDegree + ↑q.natTrailingDegree
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem bound_of_shell_of_norm_map_coord_zero (f : MultilinearMap 𝕜 E G)
    (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f m‖ = 0)
    {ε : ι → ℝ} {C : ℝ} (hε : ∀ i, 0 < ε i) {c : ι → 𝕜} (hc : ∀ i, 1 < ‖c i‖)
    (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖)
    (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖

Proof state:
case inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0✝ : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
hδ0 : 0 < ∏ i : ι, ‖δ i‖
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
simpa [map_smul_univ, norm_smul, prod_mul_distrib, mul_left_comm C, mul_le_mul_left hδ0] using
  hf (fun i => δ i • m i) hle_δm hδm_lt

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- A bound to the norm of `f` on the line `z.re = l` induces a bound to the norm of
  `scale f l u z` on the line `z.re = 0`. -/
lemma scale_bound_left {f : ℂ → E} {l u a : ℝ} (ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a) :
    ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ↑l + z * (↑u - ↑l) ∈ re ⁻¹' {l}

Tactic:
simp [hz]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ (z : ℂ), z.re = 0 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ a

Tactic:
intro z hz

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ‖f (↑l + z * (↑u - ↑l))‖ ≤ a

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ‖f (↑l + z * (↑u - ↑l))‖ ≤ a

Tactic:
exact ha (↑l + z * (↑u - ↑l)) (by simp [hz])

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a

Tactic:
simp only [mem_preimage, mem_singleton_iff, scale, smul_eq_mul]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ (z : ℂ), z.re = 0 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ a
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma negMulLog_mul (x y : ℝ) : negMulLog (x * y) = y * negMulLog x + x * negMulLog y

Proof state:
case neg
x y : ℝ
hx : ¬x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
by_cases hy : y = 0

Result:
case pos
x y : ℝ
hx : ¬x = 0
hy : y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Proof state:
x y : ℝ
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
by_cases hx : x = 0

Result:
case pos
x y : ℝ
hx : x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

case neg
x y : ℝ
hx : ¬x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Proof state:
x y : ℝ
⊢ (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog

Tactic:
simp only [negMulLog, neg_mul, neg_add_rev]

Result:
x y : ℝ
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Proof state:
case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
ring

Result:
no goals

Proof state:
case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
rw [log_mul hx hy]

Result:
case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)

Proof state:
case pos
x y : ℝ
hx : x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
simp [hx]

Result:
no goals

Proof state:
case pos
x y : ℝ
hx : ¬x = 0
hy : y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
simp [hy]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem Nodup.rotate_congr {l : List α} (hl : l.Nodup) (hn : l ≠ []) (i j : ℕ)
    (h : l.rotate i = l.rotate j) : i % l.length = j % l.length

Proof state:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate i = l.rotate j
⊢ i % l.length = j % l.length

Tactic:
rw [← rotate_mod l i, ← rotate_mod l j] at h

Result:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length

Proof state:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length

Tactic:
simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj,
  hl.getElem_inj_iff, Fin.ext_iff] using congr_arg head? h

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem mul_one (x : R[S⁻¹]) : x * 1 = x

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ ↑1 * r = r * ↑1

Tactic:
simp

Result:
no goals

Proof state:
case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 1 = r /ₒ s

Tactic:
simp [OreLocalization.one_def, oreDiv_mul_char r (1 : R) s (1 : S) r 1 (by simp)]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 1 = x

Tactic:
induction' x with r s

Result:
case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 1 = r /ₒ s
-- Mathlib/Algebra/Polynomial/EraseLead.lean
lemma natDegree_eraseLead_add_one (h : f.nextCoeff ≠ 0) :
    f.eraseLead.natDegree + 1 = f.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree

Tactic:
exact natDegree_pos_of_nextCoeff_ne_zero h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree + 1 = f.natDegree

Tactic:
rw [natDegree_eraseLead h, tsub_add_cancel_of_le]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree
-- Mathlib/Data/Int/Init.lean
@[simp, nolint simpNF] lemma natCast_nonpos_iff {n : ℕ} : (n : ℤ) ≤ 0 ↔ n = 0

Proof state:
n : ℕ
⊢ ↑n ≤ 0 ↔ n = 0

Tactic:
omega

Result:
no goals