harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isRat_pow {α} [Ring α] {f : α → ℕ → α} {a : α} {an cn : ℤ} {ad b b' cd : ℕ} :
    f = HPow.hPow → IsRat a an ad → IsNat b b' →
    Int.pow an b' = cn → Nat.pow ad b' = cd →
    IsRat (f a b) cn cd

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
rw [← Nat.cast_pow] at this

Result:
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Proof state:
case eq
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ (↑an * ⅟↑ad) ^ b = ↑(an ^ b) * ⅟↑(ad ^ b)

Tactic:
simp [invOf_pow, Commute.mul_pow]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
f : α → ℕ → α
a : α
an cn : ℤ
ad b b' cd : ℕ
⊢ f = HPow.hPow → IsRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsRat (f a b) cn cd

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)

Result:
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
have := invertiblePow (ad:α) b

Result:
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
use this

Result:
case eq
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ (↑an * ⅟↑ad) ^ b = ↑(an ^ b) * ⅟↑(ad ^ b)
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
lemma nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
    nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀

Proof state:
M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀

Tactic:
ext x

Result:
case h
M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀

Proof state:
case h
M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀

Tactic:
simp [mul_comm x]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem exists_mem_iterate_mem [IsFiniteMeasure μ] (hf : MeasurePreserving f μ μ)
    (hs : NullMeasurableSet s μ) (hs' : μ s ≠ 0) : ∃ x ∈ s, ∃ m ≠ 0, f^[m] x ∈ s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : μ s ≠ 0
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩

Result:
case intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : μ s ≠ 0
N : ℕ
hN : μ univ < ↑N * μ s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : μ s ≠ 0
N : ℕ
hN : μ univ < ↑N * μ s
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Ioo 0 N
hmx : f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
exact ⟨x, hx, m, hm.1.ne', hmx⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : μ s ≠ 0
N : ℕ
hN : μ univ < ↑N * μ s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hf.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure hs hN with ⟨x, hx, m, hm, hmx⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : μ s ≠ 0
N : ℕ
hN : μ univ < ↑N * μ s
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Ioo 0 N
hmx : f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
-- Mathlib/Order/LiminfLimsup.lean
theorem bliminf_antitone (h : ∀ x, p x → q x) : bliminf u f q ≤ bliminf u f p :=
  sSup_le_sSup fun a ha => ha.mono <| by tauto

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → a ≤ u x}
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem le_map_add_map_div' : f x ≤ f y + f (y / x)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (y / x)

Tactic:
simpa only [add_comm, map_div_rev, div_mul_cancel] using map_mul_le_add f (x / y) y

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : derivWithin f s x = derivWithin f t x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : s =ᶠ[𝓝 x] t
⊢ derivWithin f s x = derivWithin f t x

Tactic:
simp only [derivWithin, fderivWithin_congr_set h]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp] lemma C_eq_zero : (C a : MvPolynomial σ R) = 0 ↔ a = 0

Proof state:
R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = 0 ↔ a = 0

Tactic:
rw [← map_zero C, C_inj]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_multiset_prod_le (m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum

Proof state:
case refine_1
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ (⇑Multiplicative.ofAdd ∘ norm) 1 = 1

Tactic:
simp only [comp_apply, norm_one', ofAdd_zero]

Result:
no goals

Proof state:
case refine_2
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
x y : E
⊢ (⇑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (⇑Multiplicative.ofAdd ∘ norm) x * (⇑Multiplicative.ofAdd ∘ norm) y

Tactic:
exact norm_mul_le' x y

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map (fun x => ‖x‖) m).sum

Tactic:
rw [← Multiplicative.ofAdd_le, ofAdd_multiset_prod, Multiset.map_map]

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ Multiplicative.ofAdd ‖m.prod‖ ≤ (Multiset.map (⇑Multiplicative.ofAdd ∘ fun x => ‖x‖) m).prod

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ Multiplicative.ofAdd ‖m.prod‖ ≤ (Multiset.map (⇑Multiplicative.ofAdd ∘ fun x => ‖x‖) m).prod

Tactic:
refine Multiset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _

Result:
case refine_1
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ (⇑Multiplicative.ofAdd ∘ norm) 1 = 1

case refine_2
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
x y : E
⊢ (⇑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (⇑Multiplicative.ofAdd ∘ norm) x * (⇑Multiplicative.ofAdd ∘ norm) y
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_self_of_one_le (h₁ : 1 ≤ x) (h₂ : y ≤ 1) : x ^ y ≤ x

Proof state:
x y : ℝ
h₁ : 1 ≤ x
h₂ : y ≤ 1
⊢ x ^ y ≤ x

Tactic:
simpa only [rpow_one] using rpow_le_rpow_of_exponent_le h₁ h₂

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem isUnit_of_sub_one_mem_jacobson_bot (r : R) (h : r - 1 ∈ jacobson (⊥ : Ideal R)) :
    IsUnit r

Proof state:
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
⊢ IsUnit r

Tactic:
obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r h

Result:
case intro
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r

Proof state:
case intro
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r

Tactic:
rw [mem_bot, sub_eq_zero, mul_comm] at hs

Result:
case intro
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : r * s = 1
⊢ IsUnit r

Proof state:
case intro
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : r * s = 1
⊢ IsUnit r

Tactic:
exact isUnit_of_mul_eq_one _ _ hs

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
x y : R
⊢ x - y ∈ ker f ↔ f x = f y

Tactic:
rw [mem_ker, map_sub, sub_eq_zero]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_le_iff {a b c : α} : a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Tactic:
simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Defs.lean
theorem finsuppProdLEquiv_apply {α β R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    (f : α × β →₀ M) (x y) : finsuppProdLEquiv R f x y = f (x, y)

Proof state:
α : Type u_7
β : Type u_8
R : Type u_9
M : Type u_10
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α × β →₀ M
x : α
y : β
⊢ (((finsuppProdLEquiv R) f) x) y = f (x, y)

Tactic:
rw [finsuppProdLEquiv, LinearEquiv.coe_mk, finsuppProdEquiv, Finsupp.curry_apply]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem mem_adjoin_simple_iff {α : E} (x : E) :
    x ∈ adjoin F {α} ↔ ∃ r s : F[X], x = aeval α r / aeval α s

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α x : E
⊢ x ∈ F⟮α⟯ ↔ ∃ r s, x = (aeval α) r / (aeval α) s

Tactic:
simp only [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
  Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring,
  Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α x : E
⊢ (∃ a a_1, (aeval α) a / (aeval α) a_1 = x) ↔ ∃ r s, x = (aeval α) r / (aeval α) s

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α x : E
⊢ (∃ a a_1, (aeval α) a / (aeval α) a_1 = x) ↔ ∃ r s, x = (aeval α) r / (aeval α) s

Tactic:
tauto

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
lemma sInf_mem_of_not_isPredPrelimit (hlim : ¬ IsPredPrelimit (sInf s)) : sInf s ∈ s

Proof state:
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
⊢ sInf s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Result:
case intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s

Proof state:
case intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt

Result:
case intro.intro.intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_twoPow {i w: Nat} :
    (twoPow w i).msb = (decide (i < w) && decide (i = w - 1))

Proof state:
i w : Nat
⊢ i < w → i = w - 1 → 0 < w

Tactic:
intros

Result:
i w : Nat
a✝¹ : i < w
a✝ : i = w - 1
⊢ 0 < w

Proof state:
i w : Nat
a✝¹ : i < w
a✝ : i = w - 1
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
⊢ (twoPow w i).msb = (decide (i < w) && decide (i = w - 1))

Tactic:
simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
  Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]

Result:
i w : Nat
⊢ i < w → i = w - 1 → 0 < w
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
theorem IsTerminal.hom_ext {X Y : C} (t : IsTerminal X) (f g : Y ⟶ X) : f = g :=
  IsLimit.hom_ext t (by simp)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f g : Y ⟶ X
⊢ ∀ (j : Discrete PEmpty.{1}), f ≫ (asEmptyCone X).π.app j = g ≫ (asEmptyCone X).π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_norm_posPart_sub (f : α →₁[μ] ℝ) :
    integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖

Tactic:
refine @isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
    (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
    (simpleFunc.denseRange one_ne_top) (isClosed_eq ?_ ?_) ?_ f

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous integral

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous fun x => ‖Lp.posPart x‖ - ‖Lp.negPart x‖

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ ∀ (a : ↥(simpleFunc ℝ 1 μ)), (fun f => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) ↑a

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous integral

Tactic:
simp only [integral]

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous ⇑integralCLM

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous ⇑integralCLM

Tactic:
exact cont _

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ integral ↑s = ‖Lp.posPart ↑s‖ - ‖Lp.negPart ↑s‖

Tactic:
norm_cast

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ ∀ (a : ↥(simpleFunc ℝ 1 μ)), (fun f => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) ↑a

Tactic:
intro s

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ integral ↑s = ‖Lp.posPart ↑s‖ - ‖Lp.negPart ↑s‖

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous fun x => ‖Lp.posPart x‖ - ‖Lp.negPart x‖

Tactic:
refine Continuous.sub (continuous_norm.comp Lp.continuous_posPart)
  (continuous_norm.comp Lp.continuous_negPart)

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖

Tactic:
exact SimpleFunc.integral_eq_norm_posPart_sub _

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem add_mul_self (x y : R) : (x + y) * (x + y) = x * x + y * y

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) * (x + y) = x * x + y * y

Tactic:
rw [← pow_two, ← pow_two, ← pow_two, add_sq]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem lt_of_eq_of_lt {f g h : CauSeq α abs} (fg : f ≈ g) (gh : g < h) : f < h

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ f < h

Tactic:
have := pos_add_limZero gh (neg_limZero fg)

Result:
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : (h - g + -(f - g)).Pos
⊢ f < h

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : (h - g + -(f - g)).Pos
⊢ f < h

Tactic:
rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma sq_lt_sq : a ^ 2 < b ^ 2 ↔ |a| < |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ a ^ 2 < b ^ 2 ↔ |a| < |b|

Tactic:
simpa only [sq_abs] using sq_lt_sq₀ (abs_nonneg a) (abs_nonneg b)

Result:
no goals
-- Mathlib/NumberTheory/SumPrimeReciprocals.lean
/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by `N` times the sum
of `1/p` over the primes `k ≤ p ≤ N`. -/
-- This needs `Mathlib.Analysis.RCLike.Basic`, so we put it here
-- instead of in `Mathlib.NumberTheory.SmoothNumbers`.
lemma Nat.roughNumbersUpTo_card_le' (N k : ℕ) :
    (roughNumbersUpTo N k).card ≤
      N * (N.succ.primesBelow \ k.primesBelow).sum (fun p ↦ (1 : ℝ) / p)

Proof state:
N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
simp_rw [Finset.mul_sum, mul_one_div]

Result:
N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ∑ x ∈ N.succ.primesBelow \ k.primesBelow, ↑N / ↑x

Proof state:
N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ∑ x ∈ N.succ.primesBelow \ k.primesBelow, ↑N / ↑x

Tactic:
exact (Nat.cast_le.mpr <| roughNumbersUpTo_card_le N k).trans <|
  (cast_sum (β := ℝ) ..) ▸ Finset.sum_le_sum fun n _ ↦ cast_div_le

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
@[simp]
lemma ofInjective_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Injective f}
    (x : LinearMap.range f) :
    f ((ofInjective f h).symm x) = x

Proof state:
case mk.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩

Tactic:
have : ⟨f y, LinearMap.mem_range_self f y⟩ = LinearEquiv.ofInjective f h y := rfl

Result:
case mk.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
this : ⟨f y, ⋯⟩ = (ofInjective f h) y
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩

Proof state:
case mk.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
this : ⟨f y, ⋯⟩ = (ofInjective f h) y
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩

Tactic:
simp [this]

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
x : ↥(LinearMap.range f)
⊢ f ((ofInjective f h).symm x) = ↑x

Tactic:
obtain ⟨-, ⟨y, rfl⟩⟩ := x

Result:
case mk.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩
-- Mathlib/Data/Finset/Sigma.lean
theorem sigmaLift_mono (h : ∀ ⦃i⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b) (a : Σi, α i) (b : Σi, β i) :
    sigmaLift f a b ⊆ sigmaLift g a b

Proof state:
case intro.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
ha : a.fst = x.fst
hb : b.fst = x.fst
hx : x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
exact ⟨ha, hb, h hx⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ⊆ sigmaLift g a b

Tactic:
rintro x hx

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
obtain ⟨ha, hb, hx⟩ := hx

Result:
case intro.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
ha : a.fst = x.fst
hb : b.fst = x.fst
hx : x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b

Tactic:
rw [mem_sigmaLift] at hx ⊢

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurable_derivWithin_Ioi [MeasurableSpace F] [BorelSpace F] :
    Measurable fun x => derivWithin f (Ioi x) x

Proof state:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
⊢ Measurable fun x => derivWithin f (Ioi x) x

Tactic:
simpa [derivWithin_Ioi_eq_Ici] using measurable_derivWithin_Ici f

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Restriction.lean
@[reassoc]
lemma restriction_d_eq {i j : ι} {i' j' : ι'} (hi : e.f i = i') (hj : e.f j = j') :
    (K.restriction e).d i j = (K.restrictionXIso e hi).hom ≫ K.d i' j' ≫
      (K.restrictionXIso e hj).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
⊢ (K.restriction e).d i j = (K.restrictionXIso e ⋯).hom ≫ K.d (e.f i) (e.f j) ≫ (K.restrictionXIso e ⋯).inv

Tactic:
simp [restrictionXIso]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
i' j' : ι'
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.restriction e).d i j = (K.restrictionXIso e hi).hom ≫ K.d i' j' ≫ (K.restrictionXIso e hj).inv

Tactic:
subst hi hj

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
⊢ (K.restriction e).d i j = (K.restrictionXIso e ⋯).hom ≫ K.d (e.f i) (e.f j) ≫ (K.restrictionXIso e ⋯).inv