harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem d_of {G : Type u} {n : ℕ} (c : Fin (n + 1) → G) :
    d k G n (Finsupp.single c 1) =
      Finset.univ.sum fun p : Fin (n + 1) =>
        Finsupp.single (c ∘ p.succAbove) ((-1 : k) ^ (p : ℕ))

Proof state:
k : Type u
inst✝ : CommRing k
G : Type u
n : ℕ
c : Fin (n + 1) → G
⊢ (d k G n) (single c 1) = ∑ p : Fin (n + 1), single (c ∘ p.succAbove) ((-1) ^ ↑p)

Tactic:
simp [d]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_eq_empty_iff (v : Vector α n) : v.toArray = #[] ↔ n = 0

Proof state:
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ n = 0 → { toArray := v, size_toArray := h }.toArray = #[]

Tactic:
rintro rfl

Result:
α : Type u_1
v : Array α
h : v.size = 0
⊢ { toArray := v, size_toArray := h }.toArray = #[]

Proof state:
α : Type u_1
v : Array α
h : v.size = 0
⊢ { toArray := v, size_toArray := h }.toArray = #[]

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
h : #[].size = n
⊢ n = 0

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
⊢ v.toArray = #[] ↔ n = 0

Tactic:
rcases v with ⟨v, h⟩

Result:
case mk
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ { toArray := v, size_toArray := h }.toArray = #[] ↔ n = 0

Proof state:
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ { toArray := v, size_toArray := h }.toArray = #[] → n = 0

Tactic:
rintro rfl

Result:
α : Type u_1
n : Nat
h : #[].size = n
⊢ n = 0

Proof state:
case mk
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ { toArray := v, size_toArray := h }.toArray = #[] ↔ n = 0

Tactic:
exact ⟨by rintro rfl; simp_all, by rintro rfl; simpa using h⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_def' : gauge s x = sInf {r ∈ Set.Ioi (0 : ℝ) | r⁻¹ • x ∈ s}

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
r : ℝ
⊢ 0 < r ∧ x ∈ r • s ↔ r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s

Tactic:
exact and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
⊢ gauge s x = sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Tactic:
congrm sInf {r | ?_}

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
r : ℝ
⊢ 0 < r ∧ x ∈ r • s ↔ r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_one_sub_nth_order' (n : ℕ) {t : R} (ht : ‖t‖ < 1) :
    inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) :=
  have := _root_.summable_geometric_of_norm_lt_one ht
  calc inverse (1 - t) = ∑' i : ℕ, t ^ i := inverse_one_sub t ht
    _ = ∑ i ∈ range n, t ^ i + ∑' i : ℕ, t ^ (i + n) := (sum_add_tsum_nat_add _ this).symm
    _ = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i ∈ range n, t ^ i + ∑' (i : ℕ), t ^ (i + n) = ∑ i ∈ range n, t ^ i + t ^ n * inverse (1 - t)

Tactic:
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_triangle4_right (x₁ y₁ x₂ y₂ : α) :
    dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁

Tactic:
apply dist_triangle4

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

Tactic:
rw [add_right_comm, dist_comm y₁]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_two : W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 2 = ↑1 + 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
rw [show 2 = ((1 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_two, if_neg Nat.not_even_one, Ψ₂Sq,
  preΨ'_three, preΨ'_one, if_neg Nat.not_even_one, Ψ₃]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (4 * X ^ 3 + C W.b₂ * X ^ 2 + 2 * C W.b₄ * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - 2 * C W.b₆ * X - C W.b₈

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
C_simp

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (4 * X ^ 3 + C W.b₂ * X ^ 2 + 2 * C W.b₄ * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - 2 * C W.b₆ * X - C W.b₈
-- Mathlib/Order/Filter/Partial.lean
theorem pmap_res (l : Filter α) (s : Set α) (f : α → β) :
    pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)

Proof state:
case h
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)

Tactic:
simp only [PFun.core_res, mem_pmap, mem_map, mem_inf_principal, imp_iff_not_or]

Result:
case h
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l

Proof state:
case h
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)

Tactic:
ext t

Result:
case h
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
-- Mathlib/.lake/packages/batteries/Batteries/Data/LazyList.lean
theorem mem_cons {α} (x y : α) (ys : Thunk (LazyList α)) :
    x ∈ @LazyList.cons α y ys ↔ x = y ∨ x ∈ ys.get

Proof state:
α : Type u_1
x y : α
ys : Thunk (LazyList α)
⊢ x ∈ cons y ys ↔ x = y ∨ x ∈ ys.get

Tactic:
simp [Membership.mem, LazyList.Mem]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- The topological sum of `ZetaAsymptotics.term (n + 1) 1` over all `n : ℕ` is `1 - γ`. This is
proved by directly evaluating the sum of the first `N` terms and using the limit definition of `γ`.
-/
lemma term_tsum_one : HasSum (fun n ↦ term (n + 1) 1) (1 - γ)

Proof state:
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))

Tactic:
show Tendsto (fun N ↦ term_sum 1 N) atTop _

Result:
⊢ Tendsto (fun N => term_sum 1 N) atTop (𝓝 (1 - γ))

Proof state:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(↑(harmonic (n + 1)) - log ↑(n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)

Tactic:
push_cast

Result:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(↑(harmonic (n + 1)) - log (↑n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)

Proof state:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
⊢ Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))

Tactic:
refine this.congr' (Eventually.of_forall (fun n ↦ ?_))

Result:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(eulerMascheroniSeq' ∘ fun a => a + 1) n = (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) n

Proof state:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(eulerMascheroniSeq' ∘ fun a => a + 1) n = (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) n

Tactic:
simp_rw [Function.comp_apply, eulerMascheroniSeq', reduceCtorEq, if_false]

Result:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(↑(harmonic (n + 1)) - log ↑(n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)

Proof state:
⊢ Tendsto (fun N => term_sum 1 N) atTop (𝓝 (1 - γ))

Tactic:
simp_rw [term_sum_one, sub_eq_neg_add]

Result:
⊢ Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1) + 1) atTop (𝓝 (-γ + 1))

Proof state:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(↑(harmonic (n + 1)) - log (↑n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)

Tactic:
abel

Result:
no goals

Proof state:
⊢ Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1) + 1) atTop (𝓝 (-γ + 1))

Tactic:
refine Tendsto.add ?_ tendsto_const_nhds

Result:
⊢ Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))

Proof state:
⊢ Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))

Tactic:
have := (tendsto_eulerMascheroniSeq'.comp (tendsto_add_atTop_nat 1)).neg

Result:
this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))
⊢ Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))

Proof state:
⊢ HasSum (fun n => term (n + 1) 1) (1 - γ)

Tactic:
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) 1)]

Result:
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
    l₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p

Proof state:
α : Type u_1
l₂ l₁ : List α
p : α → Bool
⊢ l₁ <+ filter p l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filter p l'

Tactic:
simp only [← filterMap_eq_filter, sublist_filterMap_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α} :
    (m.insertMany l).contains k = (m.contains k || (l.map Sigma.fst).contains k)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k : α
⊢ (m.insertMany l).contains k = (m.contains k || (List.map Sigma.fst l).contains k)

Tactic:
simp_to_raw using Raw₀.contains_insertMany_list

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem hom_ext (h : Opens.IsBasis (Set.range B))
    {α β : F ⟶ F'.1} (he : ∀ i, α.app (op (B i)) = β.app (op (B i))) : α = β

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
⊢ α = β

Tactic:
apply (restrictHomEquivHom F F' h).symm.injective

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
⊢ (restrictHomEquivHom F F' h).symm α = (restrictHomEquivHom F F' h).symm β

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
⊢ (restrictHomEquivHom F F' h).symm α = (restrictHomEquivHom F F' h).symm β

Tactic:
ext i

Result:
case a.w.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ ((restrictHomEquivHom F F' h).symm α).app i = ((restrictHomEquivHom F F' h).symm β).app i

Proof state:
case a.w.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ ((restrictHomEquivHom F F' h).symm α).app i = ((restrictHomEquivHom F F' h).symm β).app i

Tactic:
exact he i.unop

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
lemma isNilpotent_pow_X_mul_C_of_isNilpotent (n : ℕ) (hnil : IsNilpotent r) :
    IsNilpotent (X ^ n * (C r))

Proof state:
R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (C r * X ^ n)

Tactic:
exact isNilpotent_C_mul_pow_X_of_isNilpotent n hnil

Result:
no goals

Proof state:
R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (X ^ n * C r)

Tactic:
rw [commute_X_pow]

Result:
R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (C r * X ^ n)
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma divInt_one (n : ℤ) : n /. 1 = n

Proof state:
n : ℤ
⊢ n /. 1 = ↑n

Tactic:
simp [divInt, mkRat, normalize]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem isInducing_nhds : IsInducing (𝓝 : X → Filter X) :=
  isInducing_iff_nhds.2 fun x =>
    (nhds_def' _).trans <| by
      simp +contextual only [nhds_nhds, comap_iInf, comap_principal,
        Iic_principal, preimage_setOf_eq, ← mem_interior_iff_mem_nhds, setOf_mem_eq,
        IsOpen.interior_eq]

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
x : X
⊢ ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 s = comap 𝓝 (𝓝 (𝓝 x))

Tactic:
simp +contextual only [nhds_nhds, comap_iInf, comap_principal,
  Iic_principal, preimage_setOf_eq, ← mem_interior_iff_mem_nhds, setOf_mem_eq,
  IsOpen.interior_eq]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem Machine.map_respects (g₁ : PointedMap Λ Λ') (g₂ : Λ' → Λ) {S} (ss : Supports M S)
    (f₂₁ : Function.RightInverse f₁ f₂) (g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q) :
    Respects (step M) (step (M.map f₁ f₂ g₁ g₂)) fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁ a = b

Proof state:
case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ Cfg.map f₁ g₁.f val✝ ∈ Option.map (Cfg.map f₁ g₁.f) (some val✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem range_circleMap (c : ℂ) (R : ℝ) : range (circleMap c R) = sphere c |R| :=
  calc
    range (circleMap c R) = c +ᵥ R • range fun θ : ℝ => exp (θ * I)

Proof state:
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c |R|

Tactic:
simp

Result:
no goals

Proof state:
c : ℂ
R : ℝ
⊢ range (circleMap c R) = c +ᵥ R • range fun θ => cexp (↑θ * I)

Tactic:
simp (config := { unfoldPartialApp := true }) only [← image_vadd, ← image_smul, ← range_comp,
  vadd_eq_add, circleMap, Function.comp_def, real_smul]

Result:
no goals

Proof state:
c : ℂ
R : ℝ
⊢ (c +ᵥ R • range fun θ => cexp (↑θ * I)) = sphere c |R|

Tactic:
rw [Complex.range_exp_mul_I, smul_sphere R 0 zero_le_one]

Result:
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c |R|
-- Mathlib/Algebra/Order/Round.lean
theorem round_two_inv : round (2⁻¹ : α) = 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
⊢ round 2⁻¹ = 1

Tactic:
simp only [round_eq, ← one_div, add_halves, floor_one]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem join_cons (a b : α) (s S) :
    join ((a, Seq.cons b s), S) = (a, Seq.join (Seq.cons (b, s) S))

Proof state:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match (Seq.cons b s).destruct with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)

Tactic:
rw [destruct_cons]

Result:
no goals

Proof state:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ join ((a, Seq.cons b s), S) = (a, (Seq.cons (b, s) S).join)

Tactic:
dsimp [join]

Result:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match (Seq.cons b s).destruct with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma negY_negY (x y : R) : W'.negY x (W'.negY x y) = y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x (W'.negY x y) = y

Tactic:
simp only [negY]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.mul_left (H1 : Disjoint f h) (H2 : Disjoint g h) : Disjoint (f * g) h := fun x =>
  by cases H1 x <;> cases H2 x <;> simp [*]

Proof state:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
⊢ (f * g) x = x ∨ h x = x

Tactic:
cases H1 x <;> cases H2 x <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (x.cast h)[i] = x[i]

Proof state:
w v i : Nat
h : w = v
x : BitVec w
p : i < v
⊢ (BitVec.cast h x)[i] = x[i]

Tactic:
subst h

Result:
w i : Nat
x : BitVec w
p : i < w
⊢ (BitVec.cast ⋯ x)[i] = x[i]

Proof state:
w i : Nat
x : BitVec w
p : i < w
⊢ (BitVec.cast ⋯ x)[i] = x[i]

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNRat/Lemmas.lean
lemma toNNRat_div (hp : 0 ≤ p) : toNNRat (p / q) = toNNRat p / toNNRat q

Proof state:
p q : ℚ
hp : 0 ≤ p
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem finiteMultiplicity_of_degree_pos_of_monic (hp : (0 : WithBot ℕ) < degree p) (hmp : Monic p)
    (hq : q ≠ 0) : FiniteMultiplicity p q :=
  have zn0 : (0 : R) ≠ 1 :=
    haveI := Nontrivial.of_polynomial_ne hq
    zero_ne_one
  ⟨natDegree q, fun ⟨r, hr⟩ => by
    have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
    have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
    have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
⊢ False

Tactic:
have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ False

Tactic:
have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
  simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne,
      hr0, not_false_eq_true]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ False

Tactic:
have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
  rw [← degree_eq_natDegree hp0]; exact hp

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
hp0 : p ≠ 0
hr : q = p ^ (q.natDegree + 1) * 0
⊢ False

Tactic:
simp [hq] at hr

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.Bornology.IsBounded.thickening {δ : ℝ} {E : Set X} (h : IsBounded E) :
    IsBounded (thickening δ E)

Proof state:
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Result:
case inl
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
h : Bornology.IsBounded ∅
⊢ Bornology.IsBounded (thickening δ ∅)

case inr.intro
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
⊢ Bornology.IsBounded (thickening δ E)

Proof state:
case inr.intro
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)

Tactic:
calc
  dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
  _ ≤ δ + diam E := add_le_add_right ((mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy).le _

Result:
no goals

Proof state:
case inl
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
h : Bornology.IsBounded ∅
⊢ Bornology.IsBounded (thickening δ ∅)

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
refine (isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩

Result:
case inr.intro
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma Scheme.map_basicOpen_map (r : Γ(X, U)) :
    U.ι ''ᵁ (U.toScheme.basicOpen <| U.topIso.inv r) = X.basicOpen r

Proof state:
X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.ι ''ᵁ (↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r

Tactic:
rw [Scheme.map_basicOpen, Scheme.basicOpen_res_eq, Scheme.Opens.topIso_inv,
  Scheme.basicOpen_res_eq X]

Result:
no goals