harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Ici : (Ici a).map Fin.valEmbedding = Icc ↑a (n - 1)

Proof state:
case h.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ valEmbedding a_1 = x) → ↑a ≤ x ∧ x ≤ n - 1

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mp.intro.intro
n : ℕ
a x : Fin n
hx : a ≤ x
⊢ ↑a ≤ valEmbedding x ∧ valEmbedding x ≤ n - 1

Proof state:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ici a) ↔ x ∈ Icc (↑a) (n - 1)

Tactic:
simp only [exists_prop, Embedding.coe_subtype, mem_Ici, mem_map, mem_Icc]

Result:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ valEmbedding a_1 = x) ↔ ↑a ≤ x ∧ x ≤ n - 1

Proof state:
case h.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a ≤ x ∧ x ≤ n - 1 → ∃ a_2, a ≤ a_2 ∧ valEmbedding a_2 = x

Tactic:
cases n

Result:
case h.mpr.zero
x : ℕ
a : Fin 0
⊢ ↑a ≤ x ∧ x ≤ 0 - 1 → ∃ a_2, a ≤ a_2 ∧ valEmbedding a_2 = x

case h.mpr.succ
x n✝ : ℕ
a : Fin (n✝ + 1)
⊢ ↑a ≤ x ∧ x ≤ n✝ + 1 - 1 → ∃ a_2, a ≤ a_2 ∧ valEmbedding a_2 = x

Proof state:
case h.mp.intro.intro
n : ℕ
a x : Fin n
hx : a ≤ x
⊢ ↑a ≤ valEmbedding x ∧ valEmbedding x ≤ n - 1

Tactic:
exact ⟨hx, Nat.le_sub_of_add_le <| x.2⟩

Result:
no goals

Proof state:
case h.mpr.zero
x : ℕ
a : Fin 0
⊢ ↑a ≤ x ∧ x ≤ 0 - 1 → ∃ a_2, a ≤ a_2 ∧ valEmbedding a_2 = x

Tactic:
exact Fin.elim0 a

Result:
no goals

Proof state:
n : ℕ
a : Fin n
⊢ map valEmbedding (Ici a) = Icc (↑a) (n - 1)

Tactic:
ext x

Result:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ici a) ↔ x ∈ Icc (↑a) (n - 1)

Proof state:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ valEmbedding a_1 = x) ↔ ↑a ≤ x ∧ x ≤ n - 1

Tactic:
constructor

Result:
case h.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a ≤ a_1 ∧ valEmbedding a_1 = x) → ↑a ≤ x ∧ x ≤ n - 1

case h.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a ≤ x ∧ x ≤ n - 1 → ∃ a_2, a ≤ a_2 ∧ valEmbedding a_2 = x

Proof state:
case h.mpr.succ
x n✝ : ℕ
a : Fin (n✝ + 1)
⊢ ↑a ≤ x ∧ x ≤ n✝ + 1 - 1 → ∃ a_2, a ≤ a_2 ∧ valEmbedding a_2 = x

Tactic:
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_insert_update {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) :
    ⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ s ⊔ ⨆ x_1 ∈ t, update f x s x_1 = s ⊔ ⨆ i ∈ t, f i

Tactic:
rcongr (i hi)

Result:
case e_a.e_s.h.e_s.h
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
i : α
hi : i ∈ t
⊢ update f x s i = f i

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ ⨆ i ∈ insert x t, update f x s i = s ⊔ ⨆ i ∈ t, f i

Tactic:
simp only [Finset.iSup_insert, update_self]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ s ⊔ ⨆ x_1 ∈ t, update f x s x_1 = s ⊔ ⨆ i ∈ t, f i

Proof state:
case e_a.e_s.h.e_s.h.h
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
i : α
hi : i ∈ t
⊢ i ≠ x

Tactic:
rintro rfl

Result:
case e_a.e_s.h.e_s.h.h
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
t : Finset α
f : α → β
s : β
i : α
hi : i ∈ t
hx : i ∉ t
⊢ False

Proof state:
case e_a.e_s.h.e_s.h
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
i : α
hi : i ∈ t
⊢ update f x s i = f i

Tactic:
apply update_of_ne

Result:
case e_a.e_s.h.e_s.h.h
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
i : α
hi : i ∈ t
⊢ i ≠ x

Proof state:
case e_a.e_s.h.e_s.h.h
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
t : Finset α
f : α → β
s : β
i : α
hi : i ∈ t
hx : i ∉ t
⊢ False

Tactic:
exact hx hi

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
lemma div2_bit (b n) : div2 (bit b n) = n

Proof state:
b : Bool
n : ℕ
⊢ (bit b n).div2 = n

Tactic:
rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
<;> cases b
<;> decide

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/PossibleTypes.lean
theorem List.exists_pw_disjoint_with_card {α : Type*} [Fintype α]
    {c : List ℕ} (hc : c.sum ≤ Fintype.card α) :
    ∃ o : List (List α),
      o.map length = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise List.Disjoint o

Proof state:
case h.right.right.hS
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ ∀ ⦃x : List ℕ⦄ (hx : ∀ a ∈ x, a < Fintype.card α) ⦃y : List ℕ⦄ (hy : ∀ a ∈ y, a < Fintype.card α),
    x.Disjoint y → (klift' x hx).Disjoint (klift' y hy)

Tactic:
intro u hu v hv huv

Result:
case h.right.right.hS
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
⊢ (klift' u hu).Disjoint (klift' v hv)

Proof state:
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ n < c.sum

Tactic:
rw [← mem_mem_ranges_iff_lt_sum]

Result:
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ ∃ s ∈ c.ranges, n ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_zip_right :
    ∀ {l₁ : List α} {l₂ : List β}, length l₂ ≤ length l₁ → (unzip (zip l₁ l₂)).2 = l₂
  | [], l₂, _ => by simp_all
  | l₁, [], _ => by simp
  | a :: l₁, b :: l₂, h => by
    simp only [zip_cons_cons, unzip_cons, unzip_zip_right (le_of_succ_le_succ h)]

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
x✝ : [].length ≤ l₁.length
⊢ (l₁.zip []).unzip.snd = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
l₁ : List α
b : β
l₂ : List β
h : (b :: l₂).length ≤ (a :: l₁).length
⊢ ((a :: l₁).zip (b :: l₂)).unzip.snd = b :: l₂

Tactic:
simp only [zip_cons_cons, unzip_cons, unzip_zip_right (le_of_succ_le_succ h)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₂ : List β
x✝ : l₂.length ≤ [].length
⊢ ([].zip l₂).unzip.snd = l₂

Tactic:
simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
lemma hasFiniteIntegral_toReal_iff {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x ≠ ∞) :
    HasFiniteIntegral (fun x ↦ (f x).toReal) μ ↔ ∫⁻ x, f x ∂μ ≠ ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x

Tactic:
filter_upwards [hf] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
x : α
hx : f x ≠ ⊤
⊢ ENNReal.ofReal (f x).toReal = f x

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
x : α
hx : f x ≠ ⊤
⊢ ENNReal.ofReal (f x).toReal = f x

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x
⊢ HasFiniteIntegral (fun x => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤

Tactic:
simp [hasFiniteIntegral_iff_enorm, Real.enorm_of_nonneg ENNReal.toReal_nonneg,
  lintegral_congr_ae this, lt_top_iff_ne_top]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ HasFiniteIntegral (fun x => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤

Tactic:
have : ∀ᵐ x ∂μ, .ofReal (f x).toReal = f x := by filter_upwards [hf] with x hx; simp [hx]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x
⊢ HasFiniteIntegral (fun x => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem Scheme.homOfLE_app {U V : X.Opens} (e : U ≤ V) (W : Opens V) :
    (X.homOfLE e).app W =
      X.presheaf.map (homOfLE <| X.ι_image_homOfLE_le_ι_image e W).op

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [e₃, ← Functor.map_comp]

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ X.presheaf.map
      (((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem ball_one_eq (r : ℝ) : ball (1 : E) r = { x | ‖x‖ < r } :=
  Set.ext fun a => by simp

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
a : E
⊢ a ∈ ball 1 r ↔ a ∈ {x | ‖x‖ < r}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftUnshift_units_smul {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ)
    (hn : n + a = n') (x : Rˣ) :
    (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
x : Rˣ
⊢ (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Tactic:
apply leftUnshift_smul

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
@[simp]
lemma coe_dualCoannihilator_span (s : Set (Module.Dual R M)) :
    ((span R s).dualCoannihilator : Set M) = {x | ∀ f ∈ s, f x = 0}

Proof state:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
this : ∀ (φ : Dual R M), x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ x ∈ ↑(span R s).dualCoannihilator ↔ x ∈ {x | ∀ f ∈ s, f x = 0}

Tactic:
simp only [SetLike.mem_coe, mem_dualCoannihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker, this]

Result:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
this : ∀ (φ : Dual R M), x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ (∀ φ ∈ span R s, φ ∈ LinearMap.ker ((Dual.eval R M) x)) ↔ ∀ f ∈ s, f ∈ LinearMap.ker ((Dual.eval R M) x)

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
⊢ ↑(span R s).dualCoannihilator = {x | ∀ f ∈ s, f x = 0}

Tactic:
ext x

Result:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
⊢ x ∈ ↑(span R s).dualCoannihilator ↔ x ∈ {x | ∀ f ∈ s, f x = 0}

Proof state:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
⊢ x ∈ ↑(span R s).dualCoannihilator ↔ x ∈ {x | ∀ f ∈ s, f x = 0}

Tactic:
have (φ) : x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker (Module.Dual.eval R M x) := by simp

Result:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
this : ∀ (φ : Dual R M), x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ x ∈ ↑(span R s).dualCoannihilator ↔ x ∈ {x | ∀ f ∈ s, f x = 0}

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
φ : Dual R M
⊢ x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
this : ∀ (φ : Dual R M), x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ (∀ φ ∈ span R s, φ ∈ LinearMap.ker ((Dual.eval R M) x)) ↔ ∀ f ∈ s, f ∈ LinearMap.ker ((Dual.eval R M) x)

Tactic:
exact span_le

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumsphere_reindex {m n : ℕ} (s : Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).circumsphere = s.circumsphere

Proof state:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius

Tactic:
exact (s.reindex e).circumsphere_unique_dist_eq.1.2

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumsphere = s.circumsphere

Tactic:
refine s.circumsphere_unique_dist_eq.2 _ ⟨?_, ?_⟩ <;> rw [← s.reindex_range_points e]

Result:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumsphere.center ∈ affineSpan ℝ (Set.range (s.reindex e).points)

case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius

Proof state:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumsphere.center ∈ affineSpan ℝ (Set.range (s.reindex e).points)

Tactic:
exact (s.reindex e).circumsphere_unique_dist_eq.1.1

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle x (x + y) = Real.arctan (‖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 x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h) (o.left_ne_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

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 (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

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 (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

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 x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma leOnePart_mul_oneLePart (a : α) : a⁻ᵐ * a⁺ᵐ = |a|ₘ

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = mabs a

Tactic:
exact sup_eq_left.2 <| one_le_mabs a

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ * a⁺ᵐ = mabs a

Tactic:
rw [oneLePart_def, mul_sup, mul_one, leOnePart_def, sup_mul, one_mul, inv_mul_cancel, sup_assoc,
  ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]

Result:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = mabs a
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux
    [CompleteSpace E] {f : ℝ → E} {g : ℝ → F}
    {k : Set ℝ} (l : Filter ℝ) [NeBot l] [TendstoIxxClass Icc l l]
    (hl : k ∈ l) (hd : ∀ᶠ x in l, DifferentiableAt ℝ f x) (hf : Tendsto (fun x => ‖f x‖) l atTop)
    (hfg : deriv f =O[l] g) : ¬IntegrableOn g k

Proof state:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntegrableOn g k volume
C : ℝ
C₀ : C ≥ 0
hC : IsBigOWith C l (deriv f) g
⊢ ∃ C,
    ∃ (_ : 0 ≤ C),
      ∃ s ∈ l,
        (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
          (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
            ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖

Tactic:
have h : ∀ᶠ x : ℝ × ℝ in l ×ˢ l,
    ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k :=
  (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets

Result:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntegrableOn g k volume
C : ℝ
C₀ : C ≥ 0
hC : IsBigOWith C l (deriv f) g
h : ∀ᶠ (x : ℝ × ℝ) in l ×ˢ l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k
⊢ ∃ C,
    ∃ (_ : 0 ≤ C),
      ∃ s ∈ l,
        (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
          (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
            ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sMod_lt (p : ℕ) (hp : p ≠ 0) (i : ℕ) : sMod p i < 2 ^ p - 1

Proof state:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i < 2 ^ p - 1

Tactic:
rw [← sMod_mod]

Result:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i % (2 ^ p - 1) < 2 ^ p - 1

Proof state:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i % (2 ^ p - 1) < 2 ^ p - 1

Tactic:
refine (Int.emod_lt _ (mersenne_int_ne_zero p hp)).trans_eq ?_

Result:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ |2 ^ p - 1| = 2 ^ p - 1

Proof state:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ |2 ^ p - 1| = 2 ^ p - 1

Tactic:
exact abs_of_nonneg (mersenne_int_pos hp).le

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem coe_iInf {ι : Sort*} (s : ι → ℝ≥0) : (↑(⨅ i, s i) : ℝ) = ⨅ i, ↑(s i)

Proof state:
ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(⨅ i, s i) = ⨅ i, ↑(s i)

Tactic:
rw [iInf, iInf, coe_sInf, ← Set.range_comp]

Result:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))

Proof state:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_two : hyperoperation 2 = (· * ·)

Proof state:
case h.h
m k : ℕ
⊢ hyperoperation 2 m k = m * k

Tactic:
induction' k with bn bih

Result:
case h.h.zero
m : ℕ
⊢ hyperoperation 2 m 0 = m * 0

case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ hyperoperation 2 m (bn + 1) = m * (bn + 1)

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ hyperoperation 2 m (bn + 1) = m * (bn + 1)

Tactic:
rw [hyperoperation_recursion, hyperoperation_one, bih]

Result:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ (fun x1 x2 => x1 + x2) m (m * bn) = m * (bn + 1)

Proof state:
⊢ hyperoperation 2 = fun x1 x2 => x1 * x2

Tactic:
ext m k

Result:
case h.h
m k : ℕ
⊢ hyperoperation 2 m k = m * k

Proof state:
case h.h.zero
m : ℕ
⊢ hyperoperation 2 m 0 = m * 0

Tactic:
rw [hyperoperation]

Result:
case h.h.zero
m : ℕ
⊢ 0 = m * 0

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m * 1 + m * bn = m * (bn + 1)

Tactic:
rw [← mul_add, add_comm]

Result:
no goals

Proof state:
case h.h.zero
m : ℕ
⊢ 0 = m * 0

Tactic:
exact (Nat.mul_zero m).symm

Result:
no goals

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m + m * bn = m * (bn + 1)

Tactic:
nth_rewrite 1 [← mul_one m]

Result:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m * 1 + m * bn = m * (bn + 1)

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ (fun x1 x2 => x1 + x2) m (m * bn) = m * (bn + 1)

Tactic:
dsimp only

Result:
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m + m * bn = m * (bn + 1)