harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_zpow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x

Proof state:
case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f.cycleOf x ^ Int.negSucc z) x = (f ^ Int.negSucc z) x

Tactic:
rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℤ
⊢ (f.cycleOf x ^ z) x = (f ^ z) x

Tactic:
cases z with
| ofNat z => exact cycleOf_pow_apply_self f x z
| negSucc z =>
  rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

Result:
no goals

Proof state:
case ofNat
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f.cycleOf x ^ Int.ofNat z) x = (f ^ Int.ofNat z) x

Tactic:
exact cycleOf_pow_apply_self f x z

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ ∀ (n : ℤ), (f.cycleOf x ^ n) x = (f ^ n) x

Tactic:
intro z

Result:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℤ
⊢ (f.cycleOf x ^ z) x = (f ^ z) x
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma extendToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    (extendToSucc hj F τ).map (homOfLE hi :
      ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) =
      (extendToSuccObjIso hj F τ i₁ (hi.trans hi₂)).hom ≫ F.map (homOfLE hi) ≫
      (extendToSuccObjIso hj F τ i₂ hi₂).inv

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc hj F τ).map (homOfLE hi) =
    (extendToSuccObjIso hj F τ i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (extendToSuccObjIso hj F τ i₂ hi₂).inv

Tactic:
rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_zero (p : K[X]) : RatFunc.mk p 0 = ofFractionRing (0 : FractionRing K[X])

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ RatFunc.mk p 0 = { toFractionRing := 0 }

Tactic:
rw [mk_eq_div', RingHom.map_zero, div_zero]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
lemma map_filter' (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α)
    [DecidablePred (∃ a, p a ∧ f a = ·)] :
    (s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝¹ : DecidablePred p
f : α ↪ β
s : Finset α
inst✝ : DecidablePred fun x => ∃ a, p a ∧ f a = x
⊢ map f (filter p s) = filter (fun b => ∃ a, p a ∧ f a = b) (map f s)

Tactic:
simp [Function.comp_def, filter_map, f.injective.eq_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem comp_coconePointsIsoOfNatIso_hom {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
    s.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).hom = w.hom.app j ≫ t.ι.app j

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
s : Cocone F
t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
j : J
⊢ s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom = w.hom.app j ≫ t.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem toFinset_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Fintype s] [Fintype t]
    [Fintype (image2 f s t)] : (image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset :=
  Finset.coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝³ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(image2 f s t)
⊢ ↑(image2 f s t).toFinset = ↑(image₂ f s.toFinset t.toFinset)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem HasDerivWithinAt.div (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x)
    (hx : d x ≠ 0) :
    HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') * (d x * d x ^ 2) = (c' * d x ^ 2 + -(c x * d' * d x)) * d x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x

Tactic:
convert hc.mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd) using 1

Result:
case h.e'_8
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (fun y => c y / d y) = fun y => c y * ((fun y => y⁻¹) ∘ d) y

case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / d x ^ 2 = c' * ((fun y => y⁻¹) ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / d x ^ 2 = c' * ((fun y => y⁻¹) ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')

Tactic:
field_simp

Result:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') * (d x * d x ^ 2) = (c' * d x ^ 2 + -(c x * d' * d x)) * d x ^ 2
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_sub' {f g : α → ℝ≥0∞} (hg : AEMeasurable g μ) (hg_fin : ∫⁻ a, g a ∂μ ≠ ∞)
    (h_le : g ≤ᵐ[μ] f) : ∫⁻ a, f a - g a ∂μ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

Tactic:
refine ENNReal.eq_sub_of_add_eq hg_fin ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
rw [← lintegral_add_right' _ hg]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
exact lintegral_congr_ae (h_le.mono fun x hx => tsub_add_cancel_of_le hx)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem isBounded_range_iff {f : β → α} : IsBounded (range f) ↔ ∃ C, ∀ x y, dist (f x) (f y) ≤ C :=
  isBounded_iff.trans <| by simp only [forall_mem_range]

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ range f → ∀ ⦃y : α⦄, y ∈ range f → dist x y ≤ C) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C

Tactic:
simp only [forall_mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = []

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = [] ↔ l = []

Tactic:
constructor <;> exact fun _ => match l with | [] => rfl

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih1_neg_right : IH1 x y → IH1 x (-y) :=
  fun h x₁ x₂ y' ↦ by
    rw [← neg_eq_iff_eq_neg, isOption_neg, P24_neg_right]
    apply h

Proof state:
x y : PGame
h : IH1 x y
x₁ x₂ y' : PGame
⊢ x₁.IsOption x → x₂.IsOption x → y' = -y ∨ y'.IsOption (-y) → P24 x₁ x₂ y'

Tactic:
rw [← neg_eq_iff_eq_neg, isOption_neg, P24_neg_right]

Result:
x y : PGame
h : IH1 x y
x₁ x₂ y' : PGame
⊢ x₁.IsOption x → x₂.IsOption x → -y' = y ∨ (-y').IsOption y → P24 x₁ x₂ (-y')

Proof state:
x y : PGame
h : IH1 x y
x₁ x₂ y' : PGame
⊢ x₁.IsOption x → x₂.IsOption x → -y' = y ∨ (-y').IsOption y → P24 x₁ x₂ (-y')

Tactic:
apply h

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
theorem res_π (i : ι) : res F U ≫ limit.π _ ⟨i⟩ = F.map (Opens.leSupr U i).op

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
i : ι
⊢ res F U ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := i } = F.map (leSupr U i).op

Tactic:
rw [res, limit.lift_π, Fan.mk_π_app]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n)

Proof state:
n i : Nat
⊢ (decide (i < n) && !testBit 0 i) = decide (i < n)

Tactic:
simp

Result:
no goals

Proof state:
case h₂
n i : Nat
⊢ 0 < 2 ^ n

Tactic:
exact Nat.two_pow_pos _

Result:
no goals

Proof state:
n i : Nat
⊢ (2 ^ n - 1).testBit i = decide (i < n)

Tactic:
rw [testBit_two_pow_sub_succ]

Result:
n i : Nat
⊢ (decide (i < n) && !testBit 0 i) = decide (i < n)

case h₂
n i : Nat
⊢ 0 < 2 ^ n
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsLittleO.multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
    {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i)
    (h₂ : ∃ i ∈ s, f i =o[l] g i) :
    (fun x ↦ (s.map (f · x)).prod) =o[l] (fun x ↦ (s.map (g · x)).prod)

Proof state:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) =o[l] fun x => (Multiset.map (fun x_1 => g x_1 x) s).prod

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s

Result:
case intro
α : Type u_1
l✝ : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
h₁ : ∀ i ∈ ↑l, f i =O[l✝] g i
h₂ : ∃ i ∈ ↑l, f i =o[l✝] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) ↑l).prod) =o[l✝] fun x => (Multiset.map (fun x_1 => g x_1 x) ↑l).prod

Proof state:
case intro
α : Type u_1
l✝ : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
h₁ : ∀ i ∈ ↑l, f i =O[l✝] g i
h₂ : ∃ i ∈ ↑l, f i =o[l✝] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) ↑l).prod) =o[l✝] fun x => (Multiset.map (fun x_1 => g x_1 x) ↑l).prod

Tactic:
exact mod_cast IsLittleO.listProd h₁ h₂

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem mem_closure_inv {G : Type*} [Group G] (S : Set G) (x : G) :
    x ∈ Submonoid.closure S⁻¹ ↔ x⁻¹ ∈ Submonoid.closure S

Proof state:
G : Type u_7
inst✝ : Group G
S : Set G
x : G
⊢ x ∈ closure S⁻¹ ↔ x⁻¹ ∈ closure S

Tactic:
rw [closure_inv, mem_inv]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_const (μ : FiniteMeasure Ω) (c : ℝ≥0) :
    μ.testAgainstNN (BoundedContinuousFunction.const Ω c) = c * μ.mass

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
c : ℝ≥0
⊢ μ.testAgainstNN (const Ω c) = c * μ.mass

Tactic:
simp [← ENNReal.coe_inj]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_sub' (a b : α) : toIocMod hp (a - p) b = toIocMod hp a b - p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (a - p) b = toIocMod hp a b - p

Tactic:
simpa only [one_zsmul] using toIocMod_sub_zsmul' hp a b 1

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem LieAlgebra.ad_eq_lmul_left_sub_lmul_right (A : Type v) [Ring A] [Algebra R A] :
    (ad R A : A → Module.End R A) = LinearMap.mulLeft R - LinearMap.mulRight R

Proof state:
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ ⇑(ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R

Tactic:
ext a b

Result:
case h.h
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ((ad R A) a) b = ((LinearMap.mulLeft R - LinearMap.mulRight R) a) b

Proof state:
case h.h
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ((ad R A) a) b = ((LinearMap.mulLeft R - LinearMap.mulRight R) a) b

Tactic:
simp [LieRing.of_associative_ring_bracket]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
@[simp]
lemma LSeries.term_sum_apply (n : ℕ) :
    term (∑ i ∈ S, f i) s n  = ∑ i ∈ S, term (f i) s n

Proof state:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

Tactic:
rcases eq_or_ne n 0 with hn | hn <;>
simp [hn, Finset.sum_div]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[ext]
lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) :
    W = W'

Proof state:
case h.h.h
C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
⊢ W f = W' f

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
⊢ W = W'

Tactic:
funext X Y f

Result:
case h.h.h
C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
⊢ W f = W' f
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem monic_normalize [DecidableEq R] (hp0 : p ≠ 0) : Monic (normalize p)

Proof state:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : p ≠ 0
⊢ (normalize p).Monic

Tactic:
rw [Ne, ← leadingCoeff_eq_zero, ← Ne, ← isUnit_iff_ne_zero] at hp0

Result:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ (normalize p).Monic

Proof state:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ IsUnit p.leadingCoeff

Tactic:
apply hp0

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ (normalize p).Monic

Tactic:
rw [Monic, leadingCoeff_normalize, normalize_eq_one]

Result:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ IsUnit p.leadingCoeff
-- Mathlib/Algebra/Module/DedekindDomain.lean
theorem exists_isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) :
    ∃ (P : Finset <| Ideal R) (_ : DecidableEq P) (_ : ∀ p ∈ P, Prime p) (e : P → ℕ),
      DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R)

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ e p)

Tactic:
exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
  isInternal_prime_power_torsion hM⟩

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ e p)

Tactic:
classical
exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
  isInternal_prime_power_torsion hM⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_top_of_bound {f : α → E} (hf : AEStronglyMeasurable f μ) (C : ℝ)
    (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : MemLp f ∞ μ :=
  ⟨hf, by
    rw [eLpNorm_exponent_top]
    exact eLpNormEssSup_lt_top_of_ae_bound hfC⟩

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f ⊤ μ < ⊤

Tactic:
rw [eLpNorm_exponent_top]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNormEssSup f μ < ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNormEssSup f μ < ⊤

Tactic:
exact eLpNormEssSup_lt_top_of_ae_bound hfC

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblU_smul (P : Fin 3 → R) (u : R) : W'.dblU (u • P) = u ^ 4 * W'.dblU P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblU (u • P) = u ^ 4 * W'.dblU P

Tactic:
simp only [dblU_eq, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.a₁ * (u ^ 3 * P y) * (u * P z) -
      (3 * (u ^ 2 * P x) ^ 2 + 2 * W'.a₂ * (u ^ 2 * P x) * (u * P z) ^ 2 + W'.a₄ * (u * P z) ^ 4) =
    u ^ 4 * (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.a₁ * (u ^ 3 * P y) * (u * P z) -
      (3 * (u ^ 2 * P x) ^ 2 + 2 * W'.a₂ * (u ^ 2 * P x) * (u * P z) ^ 2 + W'.a₄ * (u * P z) ^ 4) =
    u ^ 4 * (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem closedBall_add_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (a b : E) :
    closedBall a ε + ball b δ = ball (a + b) (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_comm δ]

Result:
no goals
-- Mathlib/Tactic/NormNum/RealSqrt.lean
lemma isNat_nnrealSqrt {x : ℝ≥0} {nx ny : ℕ} (h : IsNat x nx) (hy : ny * ny = nx) :
    IsNat (NNReal.sqrt x) ny := ⟨by simp [h.out, ← hy]⟩

Proof state:
x : ℝ≥0
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ sqrt x = ↑ny

Tactic:
simp [h.out, ← hy]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_zero_right (m : ℕ) : uniformBell m 0 = 1

Proof state:
m : ℕ
⊢ m.uniformBell 0 = 1

Tactic:
simp [uniformBell_eq]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem lintegral_map (κ : Kernel α β) (hf : Measurable f) (a : α) {g' : γ → ℝ≥0∞}
    (hg : Measurable g') : ∫⁻ b, g' b ∂map κ f a = ∫⁻ a, g' (f a) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
g' : γ → ℝ≥0∞
hg : Measurable g'
⊢ ∫⁻ (b : γ), g' b ∂(κ.map f) a = ∫⁻ (a : β), g' (f a) ∂κ a

Tactic:
rw [map_apply _ hf, lintegral_map hg hf]

Result:
no goals
-- Mathlib/Order/Booleanisation.lean
@[simp] lemma lift_le_comp : lift a ≤ comp b ↔ Disjoint a b := ⟨by rintro ⟨_⟩; assumption, LE.sep⟩

Proof state:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ≤ comp b → Disjoint a b

Tactic:
rintro ⟨_⟩

Result:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem Module.finrank_le_one_iff_top_isPrincipal [Module.Free K V] [Module.Finite K V] :
    finrank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal

Proof state:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ ⊤.IsPrincipal

Tactic:
rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem toOuterMeasure_uniformOfFintype_apply :
    (uniformOfFintype α).toOuterMeasure s = Fintype.card s / Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ (uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Tactic:
rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply,Fintype.card_ofFinset]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(Finset.filter (fun x => x ∈ s) Finset.univ).card / ↑Finset.univ.card =
    ↑(Finset.filter (Membership.mem s) Finset.univ).card / ↑(Fintype.card α)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
s : Set α
⊢ ↑(Finset.filter (fun x => x ∈ s) Finset.univ).card / ↑Finset.univ.card =
    ↑(Finset.filter (Membership.mem s) Finset.univ).card / ↑(Fintype.card α)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem log_two_gt_d9 : 0.6931471803 < log 2 :=
  lt_of_lt_of_le (by norm_num1) (sub_le_comm.1 (abs_sub_le_iff.1 log_two_near_10).2)

Proof state:
⊢ 0.6931471803 < 287209 / 414355 - 1 / 10 ^ 10

Tactic:
norm_num1

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
/-- The colexigraphic order is insensitive to removing the same elements from both sets. -/
lemma toColex_sdiff_le_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) :
    toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ { ofColex := s \ u } ≤ { ofColex := t \ u } ↔ { ofColex := s } ≤ { ofColex := t }

Tactic:
simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
  sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus),
  sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
/-- `Finsupp.mapRange` of a surjective function is surjective. -/
lemma mapRange_surjective (e : M → N) (he₀ : e 0 = 0) (he : Surjective e) :
    Surjective (Finsupp.mapRange (α := α) e he₀)

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Surjective (mapRange e he₀)

Tactic:
rw [← Set.range_eq_univ, range_mapRange, he.range_eq]

Result:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ {g | ∀ (i : α), g i ∈ Set.univ} = Set.univ

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ {g | ∀ (i : α), g i ∈ Set.univ} = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem union_left_comm (s t u : Finset α) : s ∪ (t ∪ u) = t ∪ (s ∪ u) :=
  ext fun _ => by simp only [mem_union, or_left_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x✝ : α
⊢ x✝ ∈ s ∪ (t ∪ u) ↔ x✝ ∈ t ∪ (s ∪ u)

Tactic:
simp only [mem_union, or_left_comm]

Result:
no goals