harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
lemma IsCaratheodory.biUnion_of_finite {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Finite)
    (h : ∀ i ∈ t, m.IsCaratheodory (s i)) :
    m.IsCaratheodory (⋃ i ∈ t, s i)

Proof state:
case intro.empty
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
h : ∀ i ∈ ↑∅, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑∅, s i)

Tactic:
simp

Result:
no goals

Proof state:
case intro.insert
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : (∀ i ∈ ↑t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ ↑t, s i)
h : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)

Tactic:
exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)

Tactic:
lift t to Finset ι using ht

Result:
case intro
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ ↑t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑t, s i)

Proof state:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)

Tactic:
classical
lift t to Finset ι using ht
induction t using Finset.induction_on with
| empty => simp
| @insert i t hi IH =>
  simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
  exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Result:
no goals

Proof state:
case intro
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ ↑t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑t, s i)

Tactic:
induction t using Finset.induction_on with
| empty => simp
| @insert i t hi IH =>
  simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
  exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Result:
no goals

Proof state:
case intro.insert
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : (∀ i ∈ ↑t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ ↑t, s i)
h : ∀ i_1 ∈ ↑(insert i t), m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (⋃ i_1 ∈ ↑(insert i t), s i_1)

Tactic:
simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢

Result:
case intro.insert
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : (∀ i ∈ ↑t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ ↑t, s i)
h : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ t → m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (s i ∪ ⋃ x ∈ t, s x)
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inrX_fstX (i j : ι) (hij : c.Rel i j) :
    inrX φ i ≫ fstX φ i j hij = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ inrX φ i ≫ fstX φ i j hij = 0

Tactic:
obtain rfl := c.next_eq' hij

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hij : c.Rel i (c.next i)
⊢ inrX φ i ≫ fstX φ i (c.next i) hij = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hij : c.Rel i (c.next i)
⊢ inrX φ i ≫ fstX φ i (c.next i) hij = 0

Tactic:
simp [inrX, fstX, dif_pos hij]

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem sepDegree_self : sepDegree F F = 1

Proof state:
F : Type u
inst✝ : Field F
⊢ sepDegree F F = 1

Tactic:
rw [sepDegree, Subsingleton.elim (separableClosure F F) ⊥, IntermediateField.rank_bot]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem fromLeftInv_eq_inv (x : S.leftInv) : (S.fromLeftInv x : M) = (x : M)⁻¹

Proof state:
M : Type u_1
inst✝ : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ ↑(S.fromLeftInv x) = (↑x)⁻¹

Tactic:
rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem covolume_eq_det {ι : Type*} [Fintype ι] [DecidableEq ι] (L : Submodule ℤ (ι → ℝ))
    [DiscreteTopology L] [IsZLattice ℝ L] (b : Basis ι ℤ L) :
    covolume L = |(Matrix.of ((↑) ∘ b)).det|

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L b)).det| = |(Matrix.of (Subtype.val ∘ ⇑b)).det|

Tactic:
congr

Result:
case e_a.e_M.h.e_6.h
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ ⇑(Basis.ofZLatticeBasis ℝ L b) = Subtype.val ∘ ⇑b

Proof state:
case e_a.e_M.h.e_6.h.h
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
x✝ : ι
⊢ (Basis.ofZLatticeBasis ℝ L b) x✝ = (Subtype.val ∘ ⇑b) x✝

Tactic:
exact b.ofZLatticeBasis_apply ℝ L _

Result:
no goals

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ 0 ≤ |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L b)).det|

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ covolume L volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|

Tactic:
rw [covolume_eq_measure_fundamentalDomain L volume (isAddFundamentalDomain b volume),
  volume_fundamentalDomain, ENNReal.toReal_ofReal (by positivity)]

Result:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L b)).det| = |(Matrix.of (Subtype.val ∘ ⇑b)).det|

Proof state:
case e_a.e_M.h.e_6.h
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ ⇑(Basis.ofZLatticeBasis ℝ L b) = Subtype.val ∘ ⇑b

Tactic:
ext1

Result:
case e_a.e_M.h.e_6.h.h
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
x✝ : ι
⊢ (Basis.ofZLatticeBasis ℝ L b) x✝ = (Subtype.val ∘ ⇑b) x✝
-- Mathlib/RingTheory/FinitePresentation.lean
theorem quotient {I : Ideal A} (h : I.FG) [FinitePresentation R A] :
    FinitePresentation R (A ⧸ I) where
  out

Proof state:
case intro.intro.refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((Ideal.Quotient.mkₐ R I).comp f).toRingHom).FG

Tactic:
refine Ideal.fg_ker_comp _ _ hf.2 ?_ hf.1

Result:
case intro.intro.refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker (Ideal.Quotient.mkₐ R I).toRingHom).FG

Proof state:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)

Result:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Proof state:
case intro.intro.refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker (Ideal.Quotient.mkₐ R I).toRingHom).FG

Tactic:
simp [h]

Result:
no goals

Proof state:
case intro.intro.refine_1
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((Ideal.Quotient.mkₐ R I).comp f)

Tactic:
exact (Ideal.Quotient.mkₐ_surjective R I).comp hf.1

Result:
no goals

Proof state:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
refine ⟨n, (Ideal.Quotient.mkₐ R I).comp f, ?_, ?_⟩

Result:
case intro.intro.refine_1
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((Ideal.Quotient.mkₐ R I).comp f)

case intro.intro.refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((Ideal.Quotient.mkₐ R I).comp f).toRingHom).FG
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_eq_mulSingle {f : β → α} (b : β) (hf : ∀ b' ≠ b, f b' = 1) :
    ∏' b, f b = f b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
exact fun b' hb' ↦ hf b' (by simpa using hb')

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∏' (b : β), f b = f b

Tactic:
rw [tprod_eq_prod (s := {b}), prod_singleton]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
b' : β
hb' : b' ∉ {b}
⊢ b' ≠ b

Tactic:
simpa using hb'

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_mul {x y : RatFunc K} (hx : Polynomial.eval₂ f a (denom x) ≠ 0)
    (hy : Polynomial.eval₂ f a (denom y) ≠ 0) : eval f a (x * y) = eval f a x * eval f a y

Proof state:
case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

Tactic:
have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy

Result:
case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
theorem jacobiSum_nontrivial_inv {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum χ χ⁻¹ = -χ (-1)

Proof state:
case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬y / (1 + y) = 1

Tactic:
rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, self_eq_add_left]

Result:
case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬1 = 0

Proof state:
case refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : x ∈ univ \ {1}
⊢ (fun a x => a / (1 - a)) x hx ∈ univ \ {-1}

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢

Result:
case refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : ¬x = 1
⊢ ¬x / (1 - x) = -1
-- Mathlib/Data/ENNReal/Inv.lean
theorem exists_mem_Ioc_zpow {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (hy : 1 < y) (h'y : y ≠ ⊤) :
    ∃ n : ℤ, x ∈ Ioc (y ^ n) (y ^ (n + 1))

Proof state:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n < x ∧ x ≤ y ^ (n + 1)

Tactic:
refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)

Result:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0

Proof state:
case intro.intro.intro.intro
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Tactic:
refine ⟨n, ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

case intro.intro.intro.intro.refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)

Proof state:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using hx

Result:
no goals

Proof state:
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ⊤
hy : 1 < y
h'y : y ≠ ⊤
⊢ ∃ n, x ∈ Ioc (y ^ n) (y ^ (n + 1))

Tactic:
lift x to ℝ≥0 using h'x

Result:
case intro
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (y ^ n) (y ^ (n + 1))

Proof state:
case intro.intro
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Tactic:
have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'

Result:
case intro.intro
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Proof state:
case intro.intro.intro.intro.refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

Result:
no goals

Proof state:
case intro
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (y ^ n) (y ^ (n + 1))

Tactic:
lift y to ℝ≥0 using h'y

Result:
case intro.intro
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Proof state:
case intro.intro.intro.intro.refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

Result:
no goals

Proof state:
case intro.intro
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Tactic:
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) := by
  refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
  simpa only [Ne, coe_eq_zero] using hx

Result:
case intro.intro.intro.intro
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Proof state:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem one_lt_card_iff_nontrivial (α : Type*) : 1 < card α ↔ Nontrivial α

Proof state:
α : Type u_3
⊢ 1 < card α ↔ Nontrivial α

Tactic:
rw [← Cardinal.one_lt_iff_nontrivial]

Result:
α : Type u_3
⊢ 1 < card α ↔ 1 < #α

Proof state:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < toENat #α

Tactic:
simp only [ENat.card, Nat.cast_one]

Result:
no goals

Proof state:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α

Tactic:
rw [← natCast_lt_toENat_iff]

Result:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < toENat #α

Proof state:
α : Type u_3
⊢ 1 < card α ↔ 1 < #α

Tactic:
conv_rhs => rw [← Nat.cast_one]

Result:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α
-- Mathlib/Algebra/Order/Field/Power.lean
theorem Odd.zpow_nonpos_iff (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hn : Odd 0
⊢ False

Tactic:
exact Int.not_even_iff_odd.2 hn .zero

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
n : ℤ
hn : Odd n
⊢ n ≠ 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
n : ℤ
hn : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
hn : Odd 0
⊢ False
-- Mathlib/Data/Finset/Insert.lean
theorem ssubset_iff_exists_cons_subset : s ⊂ t ↔ ∃ (a : _) (h : a ∉ s), s.cons a h ⊆ t

Proof state:
case intro.intro
α : Type u_1
s t : Finset α
h : s ⊂ t
a : α
hs : a ∈ t
ht : a ∉ s
⊢ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t

Tactic:
exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
h : s ⊂ t
⊢ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t

Tactic:
obtain ⟨a, hs, ht⟩ := not_subset.1 h.2

Result:
case intro.intro
α : Type u_1
s t : Finset α
h : s ⊂ t
a : α
hs : a ∈ t
ht : a ∉ s
⊢ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t

Proof state:
α : Type u_1
s t : Finset α
⊢ s ⊂ t ↔ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t

Tactic:
refine ⟨fun h => ?_, fun ⟨a, ha, h⟩ => ssubset_of_ssubset_of_subset (ssubset_cons _) h⟩

Result:
α : Type u_1
s t : Finset α
h : s ⊂ t
⊢ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_eq_rpow {a : A} : sqrt a = a ^ (1 / 2 : ℝ)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
this : a ^ (1 / 2) = a ^ ↑(1 / 2)
⊢ sqrt a = a ^ (1 / 2)

Tactic:
rw [this, ← nnrpow_eq_rpow (by norm_num), sqrt_eq_nnrpow (A := A)]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
⊢ sqrt a = a ^ (1 / 2)

Tactic:
have : a ^ (1 / 2 : ℝ) = a ^ ((1 / 2 : ℝ≥0) : ℝ) := rfl

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
this : a ^ (1 / 2) = a ^ ↑(1 / 2)
⊢ sqrt a = a ^ (1 / 2)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
this : a ^ (1 / 2) = a ^ ↑(1 / 2)
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
/-- For two finite measures `μ ≪ ν`, the function `x ↦ klFun (μ.rnDeriv ν x).toReal` is integrable
with respect to `ν` iff `llr μ ν` is integrable with respect to `μ`. -/
lemma integrable_klFun_rnDeriv_iff (hμν : μ ≪ ν) :
    Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
    Integrable (llr μ ν) μ
⊢ Integrable (fun x => klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
convert this using 3 with x

Result:
case h.e'_1.h.e'_6.h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
    Integrable (llr μ ν) μ
x : α
⊢ klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (fun x => klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
suffices Integrable (fun x ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal
    + (1 - (μ.rnDeriv ν x).toReal)) ν ↔ Integrable (llr μ ν) μ by
  convert this using 3 with x
  rw [klFun, add_sub_assoc]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
    Integrable (llr μ ν) μ

Proof state:
case h.e'_1.h.e'_6.h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
    Integrable (llr μ ν) μ
x : α
⊢ klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)

Tactic:
rw [klFun, add_sub_assoc]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (fun x => 1 - (μ.rnDeriv ν x).toReal) ν

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
    Integrable (llr μ ν) μ

Tactic:
rw [integrable_add_iff_integrable_left', integrable_rnDeriv_mul_log_iff hμν]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (fun x => 1 - (μ.rnDeriv ν x).toReal) ν