harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem exists_seq_forall_of_frequently {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] (h : ∃ᶠ n in l, p n) :
    ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n)

Proof state:
case intro.intro
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
obtain ⟨n_to_n, h_tendsto, h_freq⟩ := subseq_forall_of_frequently hx_tendsto hx_freq

Result:
case intro.intro.intro.intro
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
n_to_n : ℕ → ℕ
h_tendsto : Tendsto (fun n => x (n_to_n n)) atTop l
h_freq : ∀ (n : ℕ), p (x (n_to_n n))
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Proof state:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
obtain ⟨x, hx_tendsto, hx_freq⟩ := h

Result:
case intro.intro
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Proof state:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
rw [frequently_iff_seq_frequently] at h

Result:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Proof state:
case intro.intro.intro.intro
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
n_to_n : ℕ → ℕ
h_tendsto : Tendsto (fun n => x (n_to_n n)) atTop l
h_freq : ∀ (n : ℕ), p (x (n_to_n n))
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
exact ⟨x ∘ n_to_n, h_tendsto, h_freq⟩

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem divInt_mul_divInt_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : n /. x * (x /. d) = n /. d

Proof state:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [divInt_mul_divInt _ _ hx hd, x.mul_comm, divInt_mul_right hx]

Result:
no goals

Proof state:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [hd]

Result:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0

Proof state:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d

Tactic:
by_cases hd : d = 0

Result:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
-- Mathlib/Algebra/Homology/Localization.lean
@[reassoc]
lemma mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app (K : HomologicalComplex C c) :
    (F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app
        ((HomotopyCategory.quotient _ _).obj K) =
      (F.mapHomologicalComplexUpToQuasiIso c).map
          ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
        (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
          (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app _ ≫
            HomologicalComplexUpToQuasiIso.Qh.map
              ((F.mapHomotopyCategoryFactors c).inv.app K)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_4, u_1} C
inst✝¹¹ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ 𝟙
        ((F.mapHomologicalComplexUpToQuasiIso c).obj
          (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient C c).obj K))) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        𝟙
          (HomologicalComplexUpToQuasiIso.Qh.obj
            ((HomotopyCategory.quotient D c).obj
              ((F.mapHomologicalComplex c).obj ((HomotopyCategory.quotient C c).obj K).as))) =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)

Tactic:
simp only [Category.comp_id, Category.id_comp]

Result:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_4, u_1} C
inst✝¹¹ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem extend_Z_bilin_aux (x₀ : α) (y₁ : δ) : ∃ U₂ ∈ comap e (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂,
    (fun p : β × δ => φ p.1 p.2) (x' - x, y₁) ∈ W'

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
⊢ Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))

Tactic:
have := Tendsto.prod_mk (tendsto_sub_comap_self de x₀)
  (tendsto_const_nhds : Tendsto (fun _ : β × β => y₁) (comap ee <| 𝓝 (x₀, x₀)) (𝓝 y₁))

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
this : Tendsto (fun x => (x.2 - x.1, y₁)) (comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 0 ×ˢ 𝓝 y₁)
⊢ Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
let Nx := 𝓝 x₀

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem continuousOn_log : ContinuousOn log {0}ᶜ

Proof state:
⊢ Continuous fun x => expOrderIso.symm ⟨|↑x|, ⋯⟩

Tactic:
exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

Result:
no goals

Proof state:
⊢ Continuous fun x => log ↑x

Tactic:
conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]

Result:
⊢ Continuous fun x => expOrderIso.symm ⟨|↑x|, ⋯⟩

Proof state:
⊢ ContinuousOn log {0}ᶜ

Tactic:
simp (config := { unfoldPartialApp := true }) only [continuousOn_iff_continuous_restrict,
  restrict]

Result:
⊢ Continuous fun x => log ↑x
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma induce_union_connected {s t : Set V}
    (sconn : (G.induce s).Connected) (tconn : (G.induce t).Connected)
    (sintert : (s ∩ t).Nonempty) :
    (G.induce (s ∪ t)).Connected

Proof state:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
sintert : (s ∩ t).Nonempty
⊢ (⊤.induce (s ∪ t)).Connected

Tactic:
exact Subgraph.induce_union_connected sconn tconn sintert

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Connected
tconn : (induce t G).Connected
sintert : (s ∩ t).Nonempty
⊢ (induce (s ∪ t) G).Connected

Tactic:
rw [connected_induce_iff] at sconn tconn ⊢

Result:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
sintert : (s ∩ t).Nonempty
⊢ (⊤.induce (s ∪ t)).Connected
-- Mathlib/Data/Nat/WithBot.lean
theorem add_eq_three_iff {n m : WithBot ℕ} :
    n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0

Proof state:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 3 ↔ ⊥ = 0 ∧ m = 3 ∨ ⊥ = 1 ∧ m = 2 ∨ ⊥ = 2 ∧ m = 1 ∨ ⊥ = 3 ∧ m = 0

Tactic:
simp [WithBot.bot_add]

Result:
no goals

Proof state:
case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 3 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 3 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 3 ∧ ↑a✝ = 0

Tactic:
simp [← WithBot.coe_add, Nat.add_eq_three_iff]

Result:
no goals

Proof state:
n m : WithBot ℕ
⊢ n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0

Tactic:
cases n

Result:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 3 ↔ ⊥ = 0 ∧ m = 3 ∨ ⊥ = 1 ∧ m = 2 ∨ ⊥ = 2 ∧ m = 1 ∨ ⊥ = 3 ∧ m = 0

case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 3 ↔ ↑a✝ = 0 ∧ m = 3 ∨ ↑a✝ = 1 ∧ m = 2 ∨ ↑a✝ = 2 ∧ m = 1 ∨ ↑a✝ = 3 ∧ m = 0

Proof state:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 3 ↔ ↑a✝ = 0 ∧ m = 3 ∨ ↑a✝ = 1 ∧ m = 2 ∨ ↑a✝ = 2 ∧ m = 1 ∨ ↑a✝ = 3 ∧ m = 0

Tactic:
cases m

Result:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 3 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 3 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 3 ∧ ↑a✝ = 0

Proof state:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma toSingle₀Equiv_symm_apply_f_succ
    {C : CochainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X) (n : ℕ) :
    ((toSingle₀Equiv C X).symm f).f (n + 1) = 0

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
n : ℕ
⊢ ((C.toSingle₀Equiv X).symm f).f (n + 1) = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Basic.lean
theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
    (BitVec.ofNat n x).cast h = BitVec.ofNat m x

Proof state:
n x : Nat
⊢ BitVec.cast ⋯ (BitVec.ofNat n x) = BitVec.ofNat n x

Tactic:
rfl

Result:
no goals

Proof state:
n m : Nat
h : n = m
x : Nat
⊢ BitVec.cast h (BitVec.ofNat n x) = BitVec.ofNat m x

Tactic:
subst h

Result:
n x : Nat
⊢ BitVec.cast ⋯ (BitVec.ofNat n x) = BitVec.ofNat n x
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_mono_measure (f : α → ε) (hμν : ν ≤ μ) : eLpNorm f p ν ≤ eLpNorm f p μ

Proof state:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp [hp0]

Result:
no goals

Proof state:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Proof state:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp [hp_top, eLpNormEssSup_mono_measure f (Measure.absolutelyContinuous_of_le hμν)]

Result:
no goals

Proof state:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ

Tactic:
exact eLpNorm'_mono_measure f hμν ENNReal.toReal_nonneg

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Proof state:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Result:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_const : derivWithin (fun _ => c) s = 0

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
c : F
x✝ : 𝕜
⊢ derivWithin (fun x => c) s x✝ = 0 x✝

Tactic:
simp [derivWithin]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
c : F
⊢ derivWithin (fun x => c) s = 0

Tactic:
ext

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
c : F
x✝ : 𝕜
⊢ derivWithin (fun x => c) s x✝ = 0 x✝
-- Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
theorem padicValNat_def' {n : ℕ} (hp : p ≠ 1) (hn : 0 < n) :
    padicValNat p n = multiplicity p n

Proof state:
p n : ℕ
hp : p ≠ 1
hn : 0 < n
⊢ padicValNat p n = multiplicity p n

Tactic:
simp [padicValNat, hp, hn, multiplicity, emultiplicity, finiteMultiplicity_iff.2 ⟨hp, hn⟩]

Result:
p n : ℕ
hp : p ≠ 1
hn : 0 < n
⊢ Nat.find ⋯ = WithTop.untopD 1 ↑(Nat.find ⋯)

Proof state:
p n : ℕ
hp : p ≠ 1
hn : 0 < n
⊢ Nat.find ⋯ = WithTop.untopD 1 ↑(Nat.find ⋯)

Tactic:
convert (WithTop.untopD_coe ..).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Classical.lean
theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x

Tactic:
exact em _

Result:
no goals

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
rw [← not_exists]

Result:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem leftAdjointMate_comp_evaluation {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :
    X ◁ (ᘁf) ≫ ε_ _ _ = f ▷ _ ≫ ε_ _ _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (X ◁ ᘁf) ≫ ε_ (ᘁX) X = f ▷ ᘁY ≫ ε_ (ᘁY) Y

Tactic:
apply_fun tensorLeftHomEquiv _ (ᘁX) X _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) ((X ◁ ᘁf) ≫ ε_ (ᘁX) X) =
    (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) ((X ◁ ᘁf) ≫ ε_ (ᘁX) X) =
    (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.union (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) :
    StarConvex 𝕜 x (s ∪ t)

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
exact Or.inr (ht hy ha hb hab)

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
exact Or.inl (hs hy ha hb hab)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
⊢ StarConvex 𝕜 x (s ∪ t)

Tactic:
rintro y (hy | hy) a b ha hb hab

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem isOpen_extChartAt_target [I.Boundaryless] (x : M) : IsOpen (extChartAt I x).target

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ IsOpen (↑I.symm ⁻¹' (chartAt H x).target)

Tactic:
exact (PartialHomeomorph.open_target _).preimage I.continuous_symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ IsOpen (extChartAt I x).target

Tactic:
simp_rw [extChartAt_target, I.range_eq_univ, inter_univ]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ IsOpen (↑I.symm ⁻¹' (chartAt H x).target)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inl_isoPushout_inv (h : IsPushout f g inl inr) [HasPushout f g] :
    pushout.inl _ _ ≫ h.isoPushout.inv = inl

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inl

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ h.isoPushout.inv = inl

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inl
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_intCast_num_of_pos {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1

Proof state:
a : ℤ
ha0 : 0 < a
⊢ (↑1 / ↑a).num = 1

Tactic:
apply num_div_eq_of_coprime ha0

Result:
a : ℤ
ha0 : 0 < a
⊢ (Int.natAbs 1).Coprime a.natAbs

Proof state:
a : ℤ
ha0 : 0 < a
⊢ (Int.natAbs 1).Coprime a.natAbs

Tactic:
rw [Int.natAbs_one]

Result:
a : ℤ
ha0 : 0 < a
⊢ Nat.Coprime 1 a.natAbs

Proof state:
a : ℤ
ha0 : 0 < a
⊢ (↑a)⁻¹.num = 1

Tactic:
rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_divInt', divInt_eq_div, Nat.cast_one]

Result:
a : ℤ
ha0 : 0 < a
⊢ (↑1 / ↑a).num = 1

Proof state:
a : ℤ
ha0 : 0 < a
⊢ Nat.Coprime 1 a.natAbs

Tactic:
exact Nat.coprime_one_left _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
    BitVec.ofInt n x + BitVec.ofInt n y

Proof state:
n : Nat
x y : Int
⊢ BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y

Tactic:
apply eq_of_toInt_eq

Result:
case a
n : Nat
x y : Int
⊢ (BitVec.ofInt n (x + y)).toInt = (BitVec.ofInt n x + BitVec.ofInt n y).toInt

Proof state:
case a
n : Nat
x y : Int
⊢ (BitVec.ofInt n (x + y)).toInt = (BitVec.ofInt n x + BitVec.ofInt n y).toInt

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem subset_mapRange_neLocus [∀ a, DecidableEq (N a)] [∀ a, DecidableEq (M a)] (f g : Π₀ a, N a)
    {F : ∀ a, N a → M a} (F0 : ∀ a, F a 0 = 0) :
    (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g := fun a ↦ by
  simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg (F a)

Proof state:
α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → a ∈ f.neLocus g

Tactic:
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg (F a)

Result:
no goals