harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem orderOf_a_one : orderOf (a 1 : QuaternionGroup n) = 2 * n

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False

Tactic:
injection h1 with h2

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False

Tactic:
exact absurd h2.symm (orderOf_pos _).ne

Result:
no goals

Proof state:
case inl

⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1

Tactic:
intro n h

Result:
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1

Proof state:
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0

Tactic:
apply mt a.inj

Result:
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False

Tactic:
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False

Tactic:
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False

Proof state:
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1

Tactic:
rw [one_def, a_one_pow]

Result:
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False

Tactic:
rw [a_one_pow] at h1

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False

Proof state:
n : ℕ
⊢ orderOf (a 1) = 2 * n

Tactic:
rcases eq_zero_or_neZero n with hn | hn

Result:
case inl
n : ℕ
hn : n = 0
⊢ orderOf (a 1) = 2 * n

case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n

Proof state:
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n

Tactic:
apply (Nat.le_of_dvd
  (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left

Result:
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n

Proof state:
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0

Tactic:
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero

Result:
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0

Proof state:
case inl

⊢ orderOf (a 1) = 2 * 0

Tactic:
simp_rw [mul_zero, orderOf_eq_zero_iff']

Result:
case inl

⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1

Proof state:
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n

Tactic:
intro h

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False

Proof state:
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0

Tactic:
simpa using h.ne'

Result:
no goals

Proof state:
case inl
n : ℕ
hn : n = 0
⊢ orderOf (a 1) = 2 * n

Tactic:
subst hn

Result:
case inl

⊢ orderOf (a 1) = 2 * 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem safe_insert_of_performRupCheck_insertRup {n : Nat} (f : DefaultFormula n)
    (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) (rupHints : Array Nat) :
    (performRupCheck (insertRupUnits f (negate c)).1 rupHints).2.2.1 = true
      →
    Limplies (PosFin n) f (f.insert c)

Proof state:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

Tactic:
rw [c'_eq_c]

Result:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_right_comm {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ}
    {f' : α → γ → δ'} {g' : δ' → β → ε} (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) :
    image₂ f (image₂ g s t) u = image₂ g' (image₂ f' s u) t :=
  coe_injective <| by
    push_cast
    exact image2_right_comm h_right_comm

Proof state:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ ↑(image₂ f (image₂ g s t) u) = ↑(image₂ g' (image₂ f' s u) t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g ↑s ↑t) ↑u = image2 g' (image2 f' ↑s ↑u) ↑t

Proof state:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g ↑s ↑t) ↑u = image2 g' (image2 f' ↑s ↑u) ↑t

Tactic:
exact image2_right_comm h_right_comm

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem mem_range_pred_of_not_isPredPrelimit (h : ¬ IsPredPrelimit a) :
    a ∈ range (pred : α → α)

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
h : ¬IsPredPrelimit a
⊢ a ∈ range pred

Tactic:
obtain ⟨b, hb⟩ := not_isPredPrelimit_iff.1 h

Result:
case intro
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
h : ¬IsPredPrelimit a
b : α
hb : ¬IsMin b ∧ pred b = a
⊢ a ∈ range pred

Proof state:
case intro
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
h : ¬IsPredPrelimit a
b : α
hb : ¬IsMin b ∧ pred b = a
⊢ a ∈ range pred

Tactic:
exact ⟨b, hb.2⟩

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem mapIdxMGo_eq_mapIdxMAuxSpec
    [LawfulMonad m] {β} (f : ℕ → α → m β) (arr : Array β) (as : List α) :
    mapIdxM.go f as arr = (arr.toList ++ ·) <$> mapIdxMAuxSpec f arr.size as

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ mapIdxM.go f (head :: tail) arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size (head :: tail)

Tactic:
simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map,
  LawfulMonad.bind_assoc, pure_bind]

Result:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ (do
      let __do_lift ← f arr.size head
      mapIdxM.go f tail (arr.push __do_lift)) =
    do
    let x ← f arr.size head
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Proof state:
case nil
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
h : [].length = 0
⊢ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : as.length = 0
⊢ as = []

Tactic:
cases as

Result:
case nil
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
h : [].length = 0
⊢ [] = []

case cons
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = 0
⊢ head✝ :: tail✝ = []

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ (do
      let __do_lift ← f arr.size head
      mapIdxM.go f tail (arr.push __do_lift)) =
    do
    let x ← f arr.size head
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Tactic:
congr

Result:
case e_a
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ (fun __do_lift => mapIdxM.go f tail (arr.push __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem piecewise_ae_eq_restrict [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :
    piecewise s f g =ᵐ[μ.restrict s] f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᶠ[ae (μ.restrict s)] f

Tactic:
rw [ae_restrict_eq hs]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᶠ[ae μ ⊓ 𝓟 s] f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᶠ[ae μ ⊓ 𝓟 s] f

Tactic:
exact (piecewise_eqOn s f g).eventuallyEq.filter_mono inf_le_right

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem valuation_LaurentSeries_equal_extension :
    (LaurentSeriesPkg K).isDenseInducing.extend Valued.v = (Valued.v : K⸨X⸩ → ℤₘ₀)

Proof state:
case hf
K : Type u_2
inst✝ : Field K
x : RatFunc K
⊢ Valued.v ((LaurentSeriesPkg K).coe x) = Valued.v x

Tactic:
erw [valuation_eq_LaurentSeries_valuation K x]

Result:
case hf
K : Type u_2
inst✝ : Field K
x : RatFunc K
⊢ Valued.v ((LaurentSeriesPkg K).coe x) = (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑x

Proof state:
case hf
K : Type u_2
inst✝ : Field K
x : RatFunc K
⊢ Valued.v ((LaurentSeriesPkg K).coe x) = (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑x

Tactic:
rfl

Result:
no goals

Proof state:
case hf
K : Type u_2
inst✝ : Field K
⊢ ∀ (x : RatFunc K), Valued.v ((LaurentSeriesPkg K).coe x) = Valued.v x

Tactic:
intro x

Result:
case hf
K : Type u_2
inst✝ : Field K
x : RatFunc K
⊢ Valued.v ((LaurentSeriesPkg K).coe x) = Valued.v x

Proof state:
K : Type u_2
inst✝ : Field K
⊢ ⋯.extend ⇑Valued.v = ⇑Valued.v

Tactic:
apply IsDenseInducing.extend_unique

Result:
case hf
K : Type u_2
inst✝ : Field K
⊢ ∀ (x : RatFunc K), Valued.v ((LaurentSeriesPkg K).coe x) = Valued.v x

case hg
K : Type u_2
inst✝ : Field K
⊢ Continuous ⇑Valued.v

Proof state:
case hg
K : Type u_2
inst✝ : Field K
⊢ Continuous ⇑Valued.v

Tactic:
exact Valued.continuous_valuation (K := K⸨X⸩)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
@[simp]
lemma ediam_eq_one [Nontrivial α] : G.ediam = 1 ↔ G = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
⊢ G = ⊤

Tactic:
ext u v

Result:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
u v : α
⊢ G.Adj u v ↔ ⊤.Adj u v

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤

Tactic:
refine ⟨fun h₁ ↦ ?_, fun h ↦ h ▸ ediam_top⟩

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
⊢ G = ⊤

Proof state:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
h₂ : 0 < G.edist u v
h₁ : G.ediam ≤ 1
⊢ G.Adj u v

Tactic:
rw [ediam_def, iSup_le_iff] at h₁

Result:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
h₂ : 0 < G.edist u v
h₁ : ∀ (i : α × α), G.edist i.1 i.2 ≤ 1
⊢ G.Adj u v

Proof state:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
u v : α
h₂ : ⊤.Adj u v
⊢ G.Adj u v

Tactic:
apply G.edist_pos_of_ne at h₂

Result:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
u v : α
h₂ : 0 < G.edist u v
⊢ G.Adj u v

Proof state:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
h₂ : 0 < G.edist u v
h₁ : ∀ (i : α × α), G.edist i.1 i.2 ≤ 1
⊢ G.Adj u v

Tactic:
exact edist_eq_one_iff_adj.mp <| le_antisymm (h₁ (u, v)) <| Order.one_le_iff_pos.mpr h₂

Result:
no goals

Proof state:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
u v : α
⊢ G.Adj u v ↔ ⊤.Adj u v

Tactic:
refine ⟨fun h ↦ h.ne, fun h₂ ↦ ?_⟩

Result:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
u v : α
h₂ : ⊤.Adj u v
⊢ G.Adj u v

Proof state:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h₁ : G.ediam = 1
u v : α
h₂ : 0 < G.edist u v
⊢ G.Adj u v

Tactic:
apply le_of_eq at h₁

Result:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
h₂ : 0 < G.edist u v
h₁ : G.ediam ≤ 1
⊢ G.Adj u v
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem tendsto_approxOn_range_L1_enorm [OpensMeasurableSpace E] {f : β → E} {μ : Measure β}
    [SeparableSpace (range f ∪ {0} : Set E)] (fmeas : Measurable f) (hf : Integrable f μ) :
    Tendsto (fun n => ∫⁻ x, ‖approxOn f fmeas (range f ∪ {0}) 0 (by simp) n x - f x‖ₑ ∂μ) atTop
      (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
n : ℕ
x : β
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
x : β
⊢ f x ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
case hμ
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})

Tactic:
filter_upwards with x using subset_closure (by simp)

Result:
no goals

Proof state:
case hi
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x => f x - 0) μ

Tactic:
simpa using hf.2

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ) atTop (𝓝 0)

Tactic:
apply tendsto_approxOn_L1_enorm fmeas

Result:
case hμ
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})

case hi
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x => f x - 0) μ
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem insert_compl_self (x : α) : insert x ({x}ᶜ : Finset α) = univ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ insert x {x}ᶜ = univ

Tactic:
rw [← compl_erase, erase_singleton, compl_empty]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem swap_mul_swap_mul_swap {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) :
    swap y z * swap x y * swap y z = swap z x

Proof state:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x

Tactic:
rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * swap y z = swap z x

Tactic:
nth_rewrite 3 [← swap_inv]

Result:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem exists_dist_eq (x z : E) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z

Proof state:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Tactic:
nth_rw 1 [← one_smul ℝ x]

Result:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Proof state:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) (1 • z) = a * dist x z

Tactic:
simp [dist_eq_norm, ← hab, add_smul, ← smul_sub, norm_smul_of_nonneg, ha, hb]

Result:
no goals

Proof state:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Tactic:
nth_rw 4 [← one_smul ℝ z]

Result:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) (1 • z) = a * dist x z

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z

Tactic:
use a • x + b • z

Result:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).head? = xs.attach.head?.map fun ⟨a, m⟩ => f a (H a m)

Proof state:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
x : α
xs : List α
ih :
  ∀ (H : ∀ (a : α), a ∈ xs → P a),
    (pmap f xs H).head? =
      Option.map
        (fun x =>
          match x with
          | ⟨a, m⟩ => f a ⋯)
        xs.attach.head?
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ (pmap f (x :: xs) H).head? =
    Option.map
      (fun x_1 =>
        match x_1 with
        | ⟨a, m⟩ => f a ⋯)
      (x :: xs).attach.head?

Tactic:
simp at ih

Result:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
x : α
xs : List α
ih : ∀ (H : ∀ (a : α), a ∈ xs → P a), (pmap f xs H).head? = Option.map (fun x => f x.val ⋯) xs.attach.head?
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ (pmap f (x :: xs) H).head? =
    Option.map
      (fun x_1 =>
        match x_1 with
        | ⟨a, m⟩ => f a ⋯)
      (x :: xs).attach.head?

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).head? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.head?

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp at ih
  simp [head?_pmap, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
x : α
xs : List α
ih : ∀ (H : ∀ (a : α), a ∈ xs → P a), (pmap f xs H).head? = Option.map (fun x => f x.val ⋯) xs.attach.head?
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ (pmap f (x :: xs) H).head? =
    Option.map
      (fun x_1 =>
        match x_1 with
        | ⟨a, m⟩ => f a ⋯)
      (x :: xs).attach.head?

Tactic:
simp [head?_pmap, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ [] → P a
⊢ (pmap f [] H).head? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      [].attach.head?

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem adjoin_le_integralClosure {x : A} (hx : IsIntegral R x) :
    Algebra.adjoin R {x} ≤ integralClosure R A

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ {x} ⊆ ↑(integralClosure R A)

Tactic:
simp only [SetLike.mem_coe, Set.singleton_subset_iff]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ x ∈ integralClosure R A

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ x ∈ integralClosure R A

Tactic:
exact hx

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ Algebra.adjoin R {x} ≤ integralClosure R A

Tactic:
rw [Algebra.adjoin_le_iff]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ {x} ⊆ ↑(integralClosure R A)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_insertMany_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
  Raw₀.get!_insertMany_list_of_mem ⟨m.1, _⟩ m.2 k_beq distinct mem

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals