harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- Useful rewrite for the absolute value of `invInterpStrip` -/
lemma norm_invInterpStrip {ε : ℝ} (hε : ε > 0) :
    ‖invInterpStrip f z ε‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ * ‖(↑ε + ↑(sSupNormIm f 1)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
rw [← ofReal_add]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖invInterpStrip f z ε‖ = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
simp only [invInterpStrip, norm_mul]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (z - 1)‖ * ‖(↑ε + ↑(sSupNormIm f 1)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (z - 1)‖ * ‖(↑ε + ↑(sSupNormIm f 1)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
repeat rw [← ofReal_add]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
repeat rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_insert [@TransCmp α cmp] {t : RBSet α cmp} :
    v' ∈ t.insert v ↔ v' ∈ t ∨ cmp v v' = .eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
h : v' ∈ t.insert v
w✝ : α
h₁ : w✝ ∈ (t.insert v).toList
h₂ : cmp v' w✝ = Ordering.eq
⊢ v' ∈ t ∨ cmp v v' = Ordering.eq

Tactic:
match mem_toList_insert.1 h₁ with
| .inl ⟨h₃, _⟩ => exact .inl <| mem_iff_mem_toList.2 ⟨_, h₃, h₂⟩
| .inr rfl => exact .inr <| OrientedCmp.cmp_eq_eq_symm.1 h₂

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
h : v' ∈ t.insert v
⊢ v' ∈ t ∨ cmp v v' = Ordering.eq

Tactic:
let ⟨_, h₁, h₂⟩ := mem_iff_mem_toList.1 h

Result:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
h : v' ∈ t.insert v
w✝ : α
h₁ : w✝ ∈ (t.insert v).toList
h₂ : cmp v' w✝ = Ordering.eq
⊢ v' ∈ t ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
w✝ : α
h₂ : cmp v' w✝ = Ordering.eq
v : α
h₃ : w✝ ∈ t.toList
right✝ : t.find? v ≠ some w✝
h : v' ∈ t.insert v
h₁ : w✝ ∈ (t.insert v).toList
⊢ v' ∈ t ∨ cmp v v' = Ordering.eq

Tactic:
exact .inl <| mem_iff_mem_toList.2 ⟨_, h₃, h₂⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
⊢ v' ∈ t.insert v ↔ v' ∈ t ∨ cmp v v' = Ordering.eq

Tactic:
refine ⟨fun h => ?_, fun | .inl h => mem_insert_of_mem _ h | .inr h => mem_insert_of_eq _ h⟩

Result:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
h : v' ∈ t.insert v
⊢ v' ∈ t ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
w✝ : α
h₂ : cmp v' w✝ = Ordering.eq
h : v' ∈ t.insert w✝
h₁ : w✝ ∈ (t.insert w✝).toList
⊢ v' ∈ t ∨ cmp w✝ v' = Ordering.eq

Tactic:
exact .inr <| OrientedCmp.cmp_eq_eq_symm.1 h₂

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem lt_natDegree_of_mem_eraseLead_support {a : ℕ} (h : a ∈ (eraseLead f).support) :
    a < f.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree

Tactic:
exact (le_natDegree_of_mem_supp a h.2).lt_of_ne h.1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a < f.natDegree

Tactic:
rw [eraseLead_support, mem_erase] at h

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_inter [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s ∩ t).Finite) : h.toFinset = hs.toFinset ∩ ht.toFinset

Proof state:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
⊢ h.toFinset = hs.toFinset ∩ ht.toFinset

Tactic:
ext

Result:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∩ ht.toFinset

Proof state:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∩ ht.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digitsAux_def (b : ℕ) (h : 2 ≤ b) (n : ℕ) (w : 0 < n) :
    digitsAux b h n = (n % b) :: digitsAux b h (n / b)

Proof state:
case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Tactic:
rw [digitsAux]

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)

Tactic:
cases n

Result:
case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Proof state:
case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

Tactic:
cases w

Result:
no goals
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem Real.isTopologicalBasis_Ioo_rat :
    @IsTopologicalBasis ℝ _ (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) b}) :=
  isTopologicalBasis_of_isOpen_of_nhds (by simp +contextual [isOpen_Ioo])
    fun a _ hav hv =>
    let ⟨_, _, ⟨hl, hu⟩, h⟩ := mem_nhds_iff_exists_Ioo_subset.mp (IsOpen.mem_nhds hv hav)
    let ⟨q, hlq, hqa⟩ := exists_rat_btwn hl
    let ⟨p, hap, hpu⟩ := exists_rat_btwn hu
    ⟨Ioo q p, by
      simp only [mem_iUnion]
      exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩, ⟨hqa, hap⟩, fun _ ⟨hqa', ha'p⟩ =>
      h ⟨hlq.trans hqa', ha'p.trans hpu⟩⟩

Proof state:
⊢ ∀ u ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, IsOpen u

Tactic:
simp +contextual [isOpen_Ioo]

Result:
no goals

Proof state:
a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ ∃ i i_1, ∃ (_ : i < i_1), Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}

Tactic:
exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩

Result:
no goals

Proof state:
a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ Ioo ↑q ↑p ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}

Tactic:
simp only [mem_iUnion]

Result:
a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ ∃ i i_1, ∃ (_ : i < i_1), Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem exists_countable_dense_no_zero_top :
    ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Proof state:
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
h : 0 ∈ s
⊢ IsBot 0

Tactic:
simp

Result:
no goals

Proof state:
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
h : ⊤ ∈ s
⊢ IsTop ⊤

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
⊢ ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s

Tactic:
exact ⟨s, s_count, s_dense, fun h => hs.1 0 (by simp) h, fun h => hs.2 ∞ (by simp) h⟩

Result:
no goals

Proof state:
⊢ ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s

Tactic:
obtain ⟨s, s_count, s_dense, hs⟩ :
  ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s :=
  exists_countable_dense_no_bot_top ℝ≥0∞

Result:
case intro.intro.intro
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
⊢ ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiag_diagonal [DecidableEq o] [DecidableEq m] (d : m × o → α) (k : o) :
    blockDiag (diagonal d) k = diagonal fun i => d (i, k) :=
  ext fun i j => by
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
    · rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
      exact Prod.fst_eq_iff.mpr

Proof state:
case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i => d (i, k)) i i

Tactic:
rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]

Result:
no goals

Proof state:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
⊢ (diagonal d).blockDiag k i j = diagonal (fun i => d (i, k)) i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i => d (i, k)) i i

case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i => d (i, k)) i j

Proof state:
case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i => d (i, k)) i j

Tactic:
rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]

Result:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j

Proof state:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j

Tactic:
exact Prod.fst_eq_iff.mpr

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem lt_of_lt_of_eq {α} [OrderedSemiring α] {a b : α} (ha : a < 0) (hb : b = 0) : a + b < 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_eq_maxPowDiv : @padicValNat = @maxPowDiv

Proof state:
case h.h
p n : ℕ
⊢ padicValNat p n = p.maxPowDiv n

Tactic:
by_cases h : 1 < p ∧ 0 < n

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n
⊢ padicValNat p n = p.maxPowDiv n

case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n)
⊢ padicValNat p n = p.maxPowDiv n

Proof state:
case neg.left.«1».hnc
p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ ¬(1 < 1 ∧ 0 < n ∧ n % 1 = 0)

Tactic:
simp

Result:
no goals

Proof state:
case neg.right
p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ n = 0 → padicValNat p n = p.maxPowDiv n

Tactic:
intro h

Result:
case neg.right
p n : ℕ
h✝ : p ≤ 1 ∨ n = 0
h : n = 0
⊢ padicValNat p n = p.maxPowDiv n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n
⊢ FiniteMultiplicity p n

Tactic:
exact Nat.finiteMultiplicity_iff.2 ⟨h.1.ne', h.2⟩

Result:
no goals

Proof state:
case neg
p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ padicValNat p n = p.maxPowDiv n

Tactic:
apply h.elim

Result:
case neg.left
p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ p ≤ 1 → padicValNat p n = p.maxPowDiv n

case neg.right
p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ n = 0 → padicValNat p n = p.maxPowDiv n

Proof state:
case neg.left.«1»
p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ padicValNat 1 n = maxPowDiv 1 n

Tactic:
dsimp [padicValNat, maxPowDiv]

Result:
case neg.left.«1»
p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ 0 = go 0 1 n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n
⊢ padicValNat p n = p.maxPowDiv n

Tactic:
rw [padicValNat_def' h.1.ne' h.2, maxPowDiv_eq_multiplicity h.1 h.2]

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n
⊢ FiniteMultiplicity p n

Proof state:
⊢ padicValNat = maxPowDiv

Tactic:
ext p n

Result:
case h.h
p n : ℕ
⊢ padicValNat p n = p.maxPowDiv n

Proof state:
case neg.left.«1»
p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ 0 = go 0 1 n

Tactic:
rw [go, if_neg]

Result:
case neg.left.«1».hnc
p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ ¬(1 < 1 ∧ 0 < n ∧ n % 1 = 0)

Proof state:
case neg.left.«0»
p n : ℕ
h✝ : 0 ≤ 1 ∨ n = 0
h : 0 ≤ 1
⊢ padicValNat 0 n = maxPowDiv 0 n

Tactic:
simp [Classical.em]

Result:
no goals

Proof state:
case neg.right
p n : ℕ
h✝ : p ≤ 1 ∨ n = 0
h : n = 0
⊢ padicValNat p n = p.maxPowDiv n

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg.left
p n : ℕ
h✝ : p ≤ 1 ∨ n = 0
h : p ≤ 1
⊢ padicValNat p n = p.maxPowDiv n

Tactic:
interval_cases p

Result:
case neg.left.«0»
p n : ℕ
h✝ : 0 ≤ 1 ∨ n = 0
h : 0 ≤ 1
⊢ padicValNat 0 n = maxPowDiv 0 n

case neg.left.«1»
p n : ℕ
h✝ : 1 ≤ 1 ∨ n = 0
h : 1 ≤ 1
⊢ padicValNat 1 n = maxPowDiv 1 n

Proof state:
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n)
⊢ padicValNat p n = p.maxPowDiv n

Tactic:
simp only [not_and_or,not_gt_eq,Nat.le_zero] at h

Result:
case neg
p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ padicValNat p n = p.maxPowDiv n

Proof state:
case neg.left
p n : ℕ
h : p ≤ 1 ∨ n = 0
⊢ p ≤ 1 → padicValNat p n = p.maxPowDiv n

Tactic:
intro h

Result:
case neg.left
p n : ℕ
h✝ : p ≤ 1 ∨ n = 0
h : p ≤ 1
⊢ padicValNat p n = p.maxPowDiv n
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.skeletonLT_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) :
    skeletonLT C m ⊆ skeletonLT C n

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
xmem : ∃ i, ↑i < m ∧ ∃ i_1, x ∈ closedCell i i_1
⊢ ∃ i, ↑i < n ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
obtain ⟨l , lltm, xmeml⟩ := xmem

Result:
case h.intro.intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
l : ℕ
lltm : ↑l < m
xmeml : ∃ i, x ∈ closedCell l i
⊢ ∃ i, ↑i < n ∧ ∃ i_1, x ∈ closedCell i i_1

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
intro x xmem

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
xmem : x ∈ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ skeletonLT C m ⊆ skeletonLT C n

Tactic:
apply union_subset_union_right

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Proof state:
case h.intro.intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
l : ℕ
lltm : ↑l < m
xmeml : ∃ i, x ∈ closedCell l i
⊢ ∃ i, ↑i < n ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩

Result:
no goals

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
xmem : x ∈ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
simp_rw [mem_iUnion, exists_prop] at xmem ⊢

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
xmem : ∃ i, ↑i < m ∧ ∃ i_1, x ∈ closedCell i i_1
⊢ ∃ i, ↑i < n ∧ ∃ i_1, x ∈ closedCell i i_1
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem compl_mem_measurableCylinders (hs : s ∈ measurableCylinders α) :
    sᶜ ∈ measurableCylinders α

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ (cylinder s S)ᶜ = cylinder s Sᶜ

Tactic:
rw [compl_cylinder]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S
⊢ ∃ s_1 S, MeasurableSet S ∧ sᶜ = cylinder s_1 S

Tactic:
obtain ⟨s, S, hS, rfl⟩ := hs

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ ∃ s_1 S_1, MeasurableSet S_1 ∧ (cylinder s S)ᶜ = cylinder s_1 S_1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ sᶜ ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders] at hs ⊢

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S
⊢ ∃ s_1 S, MeasurableSet S ∧ sᶜ = cylinder s_1 S

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ ∃ s_1 S_1, MeasurableSet S_1 ∧ (cylinder s S)ᶜ = cylinder s_1 S_1

Tactic:
refine ⟨s, Sᶜ, hS.compl, ?_⟩

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ (cylinder s S)ᶜ = cylinder s Sᶜ
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x + y) y = Real.arcsin (‖x‖ / ‖x + y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (x + y) = ↑(Real.arcsin (‖x‖ / ‖x + y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (x + y) = ↑(Real.arcsin (‖x‖ / ‖x + y‖))

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (y + x) = ↑(Real.arcsin (‖x‖ / ‖y + x‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (y + x) = ↑(Real.arcsin (‖x‖ / ‖y + x‖))

Tactic:
exact (-o).oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem derivative_zero (n : ℕ) :
    Polynomial.derivative (bernsteinPolynomial R n 0) = -n * bernsteinPolynomial R (n - 1) 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R n 0) = -↑n * bernsteinPolynomial R (n - 1) 0

Tactic:
simp [bernsteinPolynomial, Polynomial.derivative_pow]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Filter.Tendsto.max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => max (f i) a) l (𝓝 a)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝 a)

Tactic:
exact h.max_right

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i => f i ⊔ a) l (𝓝 a)

Tactic:
simp_rw [max_comm _ a]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝 a)
-- Mathlib/Topology/GDelta/Basic.lean
/-- The empty set is meagre. -/
lemma meagre_empty : IsMeagre (∅ : Set X)

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
⊢ univ ∈ residual X

Tactic:
exact Filter.univ_mem

Result:
no goals

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
⊢ IsMeagre ∅

Tactic:
rw [IsMeagre, compl_empty]

Result:
X : Type u_5
inst✝ : TopologicalSpace X
⊢ univ ∈ residual X