harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem forall_normAtPlace_eq_zero_iff {x : mixedSpace K} :
    (∀ w, normAtPlace w x = 0) ↔ x = 0

Proof state:
case refine_1.fst.h
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsReal }
⊢ x.1 w = 0.1 w

Tactic:
exact norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)

Result:
no goals

Proof state:
case refine_1
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
⊢ x = 0

Tactic:
ext w

Result:
case refine_1.fst.h
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsReal }
⊢ x.1 w = 0.1 w

case refine_1.snd.h
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsComplex }
⊢ x.2 w = 0.2 w

Proof state:
K : Type u_1
inst✝ : Field K
x : mixedSpace K
⊢ (∀ (w : InfinitePlace K), (normAtPlace w) x = 0) ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
⊢ x = 0

case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Proof state:
case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
simp_rw [h, map_zero, implies_true]

Result:
no goals

Proof state:
case refine_1.snd.h
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsComplex }
⊢ x.2 w = 0.2 w

Tactic:
exact norm_eq_zero.mp (normAtPlace_apply_of_isComplex w.prop _ ▸ h w.1)

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_ge_three_one (n : ℕ) : ∀ k : ℕ, hyperoperation (n + 3) 1 k = 1

Proof state:
case zero
k : ℕ
⊢ (fun x1 x2 => x1 ^ x2) 1 k = 1

Tactic:
dsimp

Result:
case zero
k : ℕ
⊢ 1 ^ k = 1

Proof state:
case zero
k : ℕ
⊢ 1 ^ k = 1

Tactic:
rw [one_pow]

Result:
no goals

Proof state:
case zero

⊢ ∀ (k : ℕ), hyperoperation (0 + 3) 1 k = 1

Tactic:
intro k

Result:
case zero
k : ℕ
⊢ hyperoperation (0 + 3) 1 k = 1

Proof state:
case succ.zero
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ hyperoperation (nn + 1 + 3) 1 0 = 1

Tactic:
rw [hyperoperation_ge_three_eq_one]

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ (k : ℕ), hyperoperation (n + 3) 1 k = 1

Tactic:
induction' n with nn nih

Result:
case zero

⊢ ∀ (k : ℕ), hyperoperation (0 + 3) 1 k = 1

case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ ∀ (k : ℕ), hyperoperation (nn + 1 + 3) 1 k = 1

Proof state:
case zero
k : ℕ
⊢ hyperoperation (0 + 3) 1 k = 1

Tactic:
rw [hyperoperation_three]

Result:
case zero
k : ℕ
⊢ (fun x1 x2 => x1 ^ x2) 1 k = 1

Proof state:
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ ∀ (k : ℕ), hyperoperation (nn + 1 + 3) 1 k = 1

Tactic:
intro k

Result:
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
k : ℕ
⊢ hyperoperation (nn + 1 + 3) 1 k = 1

Proof state:
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
k : ℕ
⊢ hyperoperation (nn + 1 + 3) 1 k = 1

Tactic:
cases k

Result:
case succ.zero
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ hyperoperation (nn + 1 + 3) 1 0 = 1

case succ.succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
n✝ : ℕ
⊢ hyperoperation (nn + 1 + 3) 1 (n✝ + 1) = 1

Proof state:
case succ.succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
n✝ : ℕ
⊢ hyperoperation (nn + 1 + 3) 1 (n✝ + 1) = 1

Tactic:
rw [hyperoperation_recursion, nih]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
/-- If `F` and `F ⋙ G` are equivalence of categories, then `G` is also an equivalence. -/
lemma isEquivalence_of_comp_left {E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E)
    [IsEquivalence F] [IsEquivalence (F ⋙ G)] : IsEquivalence G

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
  isoWhiskerRight F.asEquivalence.counitIso.symm G)]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence

Tactic:
exact (F.asEquivalence.symm.trans (F ⋙ G).asEquivalence).isEquivalence_functor

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getKey! k (modifyKey k f l) = if containsKey k l then k else default

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey! k (modifyKey k f l) = if containsKey k l = true then k else default

Tactic:
simp [getKey!_modifyKey, hl]

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
theorem IsBasis.isCompact_open_iff_eq_finite_iUnion {ι : Type*} (b : ι → Opens α)
    (hb : IsBasis (Set.range b)) (hb' : ∀ i, IsCompact (b i : Set α)) (U : Set α) :
    IsCompact U ∧ IsOpen U ↔ ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i

Proof state:
case h.e'_3
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i => (b i).carrier) = SetLike.coe '' range b

Tactic:
ext

Result:
case h.e'_3.h
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i => (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b

Proof state:
case hb
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i => (b i).carrier)

Tactic:
convert (config := {transparency := .default}) hb

Result:
case h.e'_3
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i => (b i).carrier) = SetLike.coe '' range b

Proof state:
case hb'
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier

Tactic:
exact hb'

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)

Tactic:
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1

Result:
case hb
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i => (b i).carrier)

case hb'
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier

Proof state:
case h.e'_3.h
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i => (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
/-- If `‖f n‖` is `O(n^x)`, then the abscissa of absolute convergence
of `f` is bounded by `x + 1`. -/
lemma LSeries.abscissaOfAbsConv_le_of_isBigO_rpow {f : ℕ → ℂ} {x : ℝ}
    (h : f =O[atTop] fun n ↦ (n : ℝ) ^ x) :
    abscissaOfAbsConv f ≤ x + 1

Proof state:
case intro.intro
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False

Tactic:
exact (LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
  |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Result:
no goals

Proof state:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Tactic:
by_contra! H

Result:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
⊢ False

Proof state:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
⊢ False

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H

Result:
case intro.intro
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False

Proof state:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ x
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Tactic:
rw [show x = x + 1 - 1 by ring] at h

Result:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Proof state:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n => ↑n ^ x
⊢ x = x + 1 - 1

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem sigma_pi_composition_eq_iff
    (u v : Σ c : Composition n, ∀ i : Fin c.length, Composition (c.blocksFun i)) :
    u = v ↔ (ofFn fun i => (u.2 i).blocks) = ofFn fun i => (v.2 i).blocks

Proof state:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ a.blocks = a'.blocks

Tactic:
have :
  map List.sum (ofFn fun i : Fin (Composition.length a) => (b i).blocks) =
    map List.sum (ofFn fun i : Fin (Composition.length a') => (b' i).blocks) := by
  rw [H]

Result:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
this : List.map sum (ofFn fun i => (b i).blocks) = List.map sum (ofFn fun i => (b' i).blocks)
⊢ a.blocks = a'.blocks

Proof state:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
H : u = v
⊢ (ofFn fun i => (u.snd i).blocks) = ofFn fun i => (v.snd i).blocks

Tactic:
rw [H]

Result:
no goals

Proof state:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ u = v ↔ (ofFn fun i => (u.snd i).blocks) = ofFn fun i => (v.snd i).blocks

Tactic:
refine ⟨fun H => by rw [H], fun H => ?_⟩

Result:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
H : (ofFn fun i => (u.snd i).blocks) = ofFn fun i => (v.snd i).blocks
⊢ u = v

Proof state:
case mk.mk
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ ⟨a, b⟩ = ⟨a, b'⟩

Tactic:
ext1

Result:
case mk.mk.fst
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ ⟨a, b⟩.fst = ⟨a, b'⟩.fst

case mk.mk.snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ HEq ⟨a, b⟩.snd ⟨a, b'⟩.snd
-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem circleTransformDeriv_bound {R : ℝ} (hR : 0 < R) {z x : ℂ} {f : ℂ → ℂ} (hx : x ∈ ball z R)
    (hf : ContinuousOn f (sphere z R)) : ∃ B ε : ℝ, 0 < ε ∧
      ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Proof state:
case intro.intro.intro.intro.intro.mk.mk.intro
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Tactic:
let V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun _ => 1) θ

Result:
case intro.intro.intro.intro.intro.mk.mk.intro
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem omega0_le_oadd (e n a) : ω ^ repr e ≤ repr (oadd e n a)

Proof state:
e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ (e.oadd n a).repr

Tactic:
refine le_trans ?_ (le_add_right _ _)

Result:
e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ ω ^ e.repr * ↑↑n

Proof state:
e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ ω ^ e.repr * ↑↑n

Tactic:
simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos (repr e) omega0_pos).2 (Nat.cast_le.2 n.2)

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Finset.untrop_sum' [LinearOrder R] [OrderTop R] (s : Finset S) (f : S → Tropical R) :
    untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf

Tactic:
simp only [Multiset.map_map, Function.comp_apply, inf_def]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)

Tactic:
convert Multiset.untrop_sum (s.val.map f)

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem toReal_laverage {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf' : ∀ᵐ x ∂μ, f x ≠ ∞) :
    (⨍⁻ x, f x ∂μ).toReal = ⨍ x, (f x).toReal ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ

Tactic:
rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
  integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2)]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem writtenInExtChartAt_chartAt_comp [ChartedSpace H H'] (x : M') {y}
    (hy : y ∈ letI := ChartedSpace.comp H H' M'; (extChartAt I x).target) :
    (letI := ChartedSpace.comp H H' M'; writtenInExtChartAt I I x (chartAt H' x) y) = y

Proof state:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
this : ChartedSpace H M' := ChartedSpace.comp H H' M'
⊢ writtenInExtChartAt I I x (↑(chartAt H' x)) y = y

Tactic:
simp_all only [mfld_simps, chartAt_comp]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I I x (↑(chartAt H' x)) y = y

Tactic:
letI := ChartedSpace.comp H H' M'

Result:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
this : ChartedSpace H M' := ChartedSpace.comp H H' M'
⊢ writtenInExtChartAt I I x (↑(chartAt H' x)) y = y
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.apply_zero_uncurry0 (f : G[×0]→L[𝕜] G') {x : Fin 0 → G} :
    ContinuousMultilinearMap.uncurry0 𝕜 G (f x) = f

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x : Fin 0 → G
⊢ uncurry0 𝕜 G (f x) = f

Tactic:
ext m

Result:
case H
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x m : Fin 0 → G
⊢ (uncurry0 𝕜 G (f x)) m = f m

Proof state:
case H
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x m : Fin 0 → G
⊢ (uncurry0 𝕜 G (f x)) m = f m

Tactic:
simp [Subsingleton.elim x m]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h))

Proof state:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
⊢ (as ++ bs).toList[i] = bs.toList[i - as.size]

Tactic:
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h

Result:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList[i] = bs.toList[i - as.size]

Proof state:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList[i] = (as.toList ++ bs.toList)[i]

Tactic:
apply List.get_of_eq

Result:
case h
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList = as.toList ++ bs.toList

Proof state:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
⊢ i < (as.toList ++ bs.toList).length

Tactic:
rwa [← length_toList, toList_append] at h

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList[i] = bs.toList[i - as.size]

Tactic:
conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]

Result:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList[i] = (as.toList ++ bs.toList)[i]

Proof state:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
⊢ (as ++ bs)[i] = bs[i - as.size]

Tactic:
simp only [← getElem_toList]

Result:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
⊢ (as ++ bs).toList[i] = bs.toList[i - as.size]

Proof state:
case h
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hle : as.size ≤ i
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList = as.toList ++ bs.toList

Tactic:
rw [toList_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_tail (l : List α) (i : Nat) (h : i < l.tail.length) :
    (tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h))

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.tail.length
⊢ l.tail[i] = l[i + 1]

Tactic:
cases l with
| nil => simp at h
| cons _ l => simp

Result:
no goals

Proof state:
α : Type ?u.110742
l : List α
i : Nat
h : i < l.tail.length
⊢ i < l.length - 1

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
i : Nat
head✝ : α
l : List α
h : i < (head✝ :: l).tail.length
⊢ (head✝ :: l).tail[i] = (head✝ :: l)[i + 1]

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
i : Nat
h : i < [].tail.length
⊢ [].tail[i] = [][i + 1]

Tactic:
simp at h

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem ofRestrict_top_c (X : PresheafedSpace C) :
    (X.ofRestrict (Opens.isOpenEmbedding ⊤)).c =
      eqToHom
        (by
          rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
          erw [Iso.inv_hom_id]
          rw [Presheaf.id_pushforward]
          dsimp)

Proof state:
case w
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (X.ofRestrict ⋯).c.app (op U✝) = (eqToHom ⋯).app (op U✝)

Tactic:
dsimp [ofRestrict]

Result:
case w
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ X.presheaf.map (⋯.adjunction.counit.app U✝).op = (eqToHom ⋯).app (op U✝)

Proof state:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (𝟭 (Presheaf C ↑X)).obj X.presheaf

Tactic:
dsimp

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ X.presheaf.map (⋯.adjunction.counit.app U✝).op = (eqToHom ⋯).app (op U✝)

Tactic:
erw [eqToHom_map, eqToHom_app]

Result:
case w.p
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op (⋯.functor.obj ((Opens.map ⊤.inclusion').obj U✝))

Proof state:
case w.p
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op (⋯.functor.obj ((Opens.map ⊤.inclusion').obj U✝))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C (𝟙 ↑X)).obj X.presheaf

Tactic:
rw [Presheaf.id_pushforward]

Result:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (𝟭 (Presheaf C ↑X)).obj X.presheaf

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (X.ofRestrict ⋯).c = eqToHom ⋯

Tactic:
ext

Result:
case w
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (X.ofRestrict ⋯).c.app (op U✝) = (eqToHom ⋯).app (op U✝)

Proof state:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj (X.restrict ⋯).presheaf

Tactic:
rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]

Result:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C ((Opens.inclusionTopIso ↑X).inv ≫ (X.ofRestrict ⋯).base)).obj X.presheaf

Proof state:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C ((Opens.inclusionTopIso ↑X).inv ≫ (X.ofRestrict ⋯).base)).obj X.presheaf

Tactic:
erw [Iso.inv_hom_id]

Result:
C : Type u_1
inst✝ : Category.{?u.71419, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C (𝟙 ↑X)).obj X.presheaf