harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addU_of_Z_eq_zero_right {P Q : Fin 3 → F} (hQz : Q z = 0) : addU P Q = 0

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ addU P Q = 0

Tactic:
rw [addU, hQz, mul_zero, div_zero, neg_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n

Proof state:
case H0
k n : Nat
km : k ∣ 0
kn : k ∣ n
⊢ k ∣ gcd 0 n

Tactic:
rw [gcd_zero_left]

Result:
case H0
k n : Nat
km : k ∣ 0
kn : k ∣ n
⊢ k ∣ n

Proof state:
case H1
k n m : Nat
a✝ : 0 < n
IH : k ∣ m % n → k ∣ n → k ∣ (m % n).gcd n
km : k ∣ n
kn : k ∣ m
⊢ k ∣ n.gcd m

Tactic:
rw [gcd_rec]

Result:
case H1
k n m : Nat
a✝ : 0 < n
IH : k ∣ m % n → k ∣ n → k ∣ (m % n).gcd n
km : k ∣ n
kn : k ∣ m
⊢ k ∣ (m % n).gcd n

Proof state:
case H1
k n m : Nat
a✝ : 0 < n
IH : k ∣ m % n → k ∣ n → k ∣ (m % n).gcd n
km : k ∣ n
kn : k ∣ m
⊢ k ∣ (m % n).gcd n

Tactic:
exact IH ((dvd_mod_iff km).2 kn) km

Result:
no goals

Proof state:
case H0
k n : Nat
km : k ∣ 0
kn : k ∣ n
⊢ k ∣ n

Tactic:
exact kn

Result:
no goals

Proof state:
k m n : Nat
⊢ k ∣ m → k ∣ n → k ∣ m.gcd n

Tactic:
induction m, n using gcd.induction with intro km kn
| H0 n => rw [gcd_zero_left]; exact kn
| H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_le_pi (θ : Angle) : θ.toReal ≤ π

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝).toReal ≤ π

Tactic:
convert toIocMod_le_right two_pi_pos _ _

Result:
case h.e'_4
x✝ : ℝ
⊢ π = -π + 2 * π

Proof state:
case h.e'_4
x✝ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring

Result:
no goals

Proof state:
θ : Angle
⊢ θ.toReal ≤ π

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝).toReal ≤ π
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma measure_sub_singularPart (μ ν : Measure α) [HaveLebesgueDecomposition μ ν]
    [IsFiniteMeasure μ] :
    μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

Tactic:
nth_rw 1 [← rnDeriv_add_singularPart μ ν]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

Tactic:
exact Measure.add_sub_cancel

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem append_nil (as : List α) : as ++ [] = as

Proof state:
case nil
α : Type u
⊢ nil ++ nil = nil

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
as : List α
⊢ as ++ nil = as

Tactic:
induction as with
| nil => rfl
| cons a as ih =>
  simp_all only [HAppend.hAppend, Append.append, List.append]

Result:
no goals

Proof state:
case cons
α : Type u
a : α
as : List α
ih : as ++ nil = as
⊢ a :: as ++ nil = a :: as

Tactic:
simp_all only [HAppend.hAppend, Append.append, List.append]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma intCast_cast_add (x y : ZMod n) : (cast (x + y) : ℤ) = (cast x + cast y) % n

Proof state:
n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x.cast + y.cast) % ↑n

Tactic:
rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderEmbedding.lean
theorem preimage_Ioo : e ⁻¹' Ioo (e x) (e y) = Ioo x y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ioo (e x) (e y) = Ioo x y

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioo (e x) (e y) ↔ x✝ ∈ Ioo x y

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioo (e x) (e y) ↔ x✝ ∈ Ioo x y

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Basic.lean
lemma eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt {x' y' : α}
    (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x')) :
    x = y ↔ x' = y'

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x y x' y' : α
ltc : x < y ↔ x' < y'
gtc : y < x ↔ y' < x'
⊢ x = y ↔ x' = y'

Tactic:
simp_rw [eq_iff_le_not_lt, ← not_lt, ltc, gtc]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_two : preNormEDS b c d 2 = 1

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 2 = 1

Tactic:
erw [preNormEDS_ofNat, preNormEDS'_two]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem lintegral_fn_integral_sub ⦃f g : α × β → E⦄ (F : E → ℝ≥0∞) (hf : Integrable f (μ.prod ν))
    (hg : Integrable g (μ.prod ν)) :
    (∫⁻ x, F (∫ y, f (x, y) - g (x, y) ∂ν) ∂μ) =
      ∫⁻ x, F ((∫ y, f (x, y) ∂ν) - ∫ y, g (x, y) ∂ν) ∂μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
    ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ

Tactic:
refine lintegral_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)

Proof state:
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y => f (a✝, y)) ν
h2g : Integrable (fun y => g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)

Tactic:
simp [integral_sub h2f h2g]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

Result:
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y => f (a✝, y)) ν
h2g : Integrable (fun y => g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey' {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} :
    (alterKey k f l).length =
      if containsKey k l && (f (getValueCast? k l)).isNone then
        l.length - 1
      else if !containsKey k l && (f (getValueCast? k l)).isSome then
        l.length + 1
      else
        l.length

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if (containsKey k l && (f (getValueCast? k l)).isNone) = true then l.length - 1
    else if (!containsKey k l && (f (getValueCast? k l)).isSome) = true then l.length + 1 else l.length

Tactic:
cases h : containsKey k l <;> split <;> split <;> simp_all [length_eraseKey, length_insertEntry]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (alterKey k f l).length =
    if (containsKey k l && (f (getValueCast? k l)).isNone) = true then l.length - 1
    else if (!containsKey k l && (f (getValueCast? k l)).isSome) = true then l.length + 1 else l.length

Tactic:
rw [alterKey]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if (containsKey k l && (f (getValueCast? k l)).isNone) = true then l.length - 1
    else if (!containsKey k l && (f (getValueCast? k l)).isSome) = true then l.length + 1 else l.length
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_exp_comp_nhds_zero {f : α → ℝ} :
    Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto f l atBot

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem multiplicity_choose_aux {p n b k : ℕ} (hp : p.Prime) (hkn : k ≤ n) :
    ∑ i ∈ Finset.Ico 1 b, n / p ^ i =
      ((∑ i ∈ Finset.Ico 1 b, k / p ^ i) + ∑ i ∈ Finset.Ico 1 b, (n - k) / p ^ i) +
        #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i} :=
  calc
    ∑ i ∈ Finset.Ico 1 b, n / p ^ i = ∑ i ∈ Finset.Ico 1 b, (k + (n - k)) / p ^ i

Proof state:
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, n / p ^ i = ∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i

Tactic:
simp only [add_tsub_cancel_of_le hkn]

Result:
no goals

Proof state:
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i =
    ∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0)

Tactic:
simp only [Nat.add_div (pow_pos hp.pos _)]

Result:
no goals

Proof state:
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) =
    ∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n - k) / p ^ i +
      #(filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))

Tactic:
simp [sum_add_distrib, sum_boole]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_find_iff (n : ℕ) : (n : PartENat) < find P ↔ ∀ m ≤ n, ¬P m

Proof state:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (h : (find P).Dom), n < (find P).get h
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H

Tactic:
specialize h H

Result:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n m : ℕ
hm : m ≤ n
H : (find P).Dom
h : n < (find P).get H
⊢ m < Nat.find H

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
⊢ ¬P m

Tactic:
by_cases H : (find P).Dom

Result:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ ¬P m

case neg
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : ¬(find P).Dom
⊢ ¬P m

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P → ∀ m ≤ n, ¬P m

Tactic:
intro h m hm

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
⊢ ¬P m

Proof state:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ ¬P m

Tactic:
apply Nat.find_min H

Result:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H

Proof state:
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : ¬(find P).Dom
⊢ ¬P m

Tactic:
exact not_exists.mp H m

Result:
no goals

Proof state:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n m : ℕ
hm : m ≤ n
H : (find P).Dom
h : n < (find P).get H
⊢ m < Nat.find H

Tactic:
exact lt_of_le_of_lt hm h

Result:
no goals

Proof state:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H

Tactic:
rw [coe_lt_iff] at h

Result:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (h : (find P).Dom), n < (find P).get h
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P ↔ ∀ m ≤ n, ¬P m

Tactic:
refine ⟨?_, lt_find P n⟩

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P → ∀ m ≤ n, ¬P m
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_div_cancel_right (a b c : G) : a / c / (b / c) = a / b

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / c / (b / c) = a / b

Tactic:
rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_le_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b))
    (hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x) : (∫ y in a..b, φ y) ≤ g b - g a

Proof state:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ ∫ (y : ℝ) in a..b, φ y ≤ g b - g a

Tactic:
rw [← neg_le_neg_iff]

Result:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y

Proof state:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y

Tactic:
convert sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg)
  φint.neg fun x hx => neg_le_neg (hφg x hx) using 1

Result:
case h.e'_3
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a

case h.e'_4
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -∫ (y : ℝ) in a..b, φ y = ∫ (y : ℝ) in a..b, (-φ) y

Proof state:
case h.e'_4
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -∫ (y : ℝ) in a..b, φ y = ∫ (y : ℝ) in a..b, (-φ) y

Tactic:
simp only [← integral_neg]

Result:
case h.e'_4
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ ∫ (x : ℝ) in a..b, -φ x = ∫ (y : ℝ) in a..b, (-φ) y

Proof state:
case h.e'_4
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ ∫ (x : ℝ) in a..b, -φ x = ∫ (y : ℝ) in a..b, (-φ) y

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a

Tactic:
abel

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.pow_right (H : IsCoprime x y) : IsCoprime x (y ^ n)

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (y ^ n)

Tactic:
rw [← Finset.card_range n, ← Finset.prod_const]

Result:
R : Type u
inst✝ : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x ∈ range n, y)

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x ∈ range n, y)

Tactic:
exact IsCoprime.prod_right fun _ _ ↦ H

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem HasBasis.nhds {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
    HasBasis (𝓝 l) p fun i => Iic (𝓟 (s i))

Proof state:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (l.lift' (Iic ∘ 𝓟)).HasBasis p fun i => Iic (𝓟 (s i))

Tactic:
exact h.lift' monotone_principal.Iic

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i => Iic (𝓟 (s i))

Tactic:
rw [nhds_eq]

Result:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (l.lift' (Iic ∘ 𝓟)).HasBasis p fun i => Iic (𝓟 (s i))
-- Mathlib/Order/Antichain.lean
theorem isAntichain_and_least_iff : IsAntichain (· ≤ ·) s ∧ IsLeast s a ↔ s = {a} :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun _ hb => h.1.eq' hb h.2.1 (h.2.2 hb)⟩, by
    rintro rfl
    exact ⟨isAntichain_singleton _ _, isLeast_singleton⟩⟩

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsAntichain (fun x1 x2 => x1 ≤ x2) {a} ∧ IsLeast {a} a

Tactic:
exact ⟨isAntichain_singleton _ _, isLeast_singleton⟩

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 => x1 ≤ x2) s ∧ IsLeast s a

Tactic:
rintro rfl

Result:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsAntichain (fun x1 x2 => x1 ≤ x2) {a} ∧ IsLeast {a} a
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_le_iff : ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
refine ⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N') → {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N'

Proof state:
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨m, hm⟩⁆ ∈ ↑N'

Tactic:
exact h x hx m hm

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N') → {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N'

Tactic:
rintro h _ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩

Result:
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨m, hm⟩⁆ ∈ ↑N'
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.dropLast_tail {α}
    {L : List α} (hL : L ≠ []) (hL' : L.head hL = L.getLast hL) : L.dropLast ~r L.tail :=
  match L with
  | [] => by simp
  | [_] => by simp
  | a :: b :: L => by
    simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'
    simp [hL', IsRotated.cons_getLast_dropLast]

Proof state:
α : Type u_1
L : List α
head✝ : α
hL : [head✝] ≠ []
hL' : [head✝].head hL = [head✝].getLast hL
⊢ [head✝].dropLast ~r [head✝].tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
L : List α
hL : [] ≠ []
hL' : [].head hL = [].getLast hL
⊢ [].dropLast ~r [].tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : (a :: b :: L).head hL = (a :: b :: L).getLast hL
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'

Result:
α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : a = (b :: L).getLast ⋯
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Proof state:
α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : a = (b :: L).getLast ⋯
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
simp [hL', IsRotated.cons_getLast_dropLast]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem cons_union (a : α) (l₁ l₂ : List α) :
    (a :: l₁) ∪ l₂ = (l₁ ∪ l₂).insert a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)

Tactic:
simp [List.union_def, foldr]

Result:
no goals
-- Mathlib/Algebra/CharP/Basic.lean
lemma intCast_eq_intCast : (a : R) = b ↔ a ≡ b [ZMOD p]

Proof state:
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

Tactic:
rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.intCast_eq_zero_iff R p, Int.modEq_iff_dvd]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDeriv_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) :
    (iteratedFDeriv 𝕜 n fun _ : E ↦ c) = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : n ≠ 0
c : F
⊢ (iteratedFDeriv 𝕜 n fun x => c) = 0

Tactic:
simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_const_of_ne hn]

Result:
no goals