harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Field/NegOnePow.lean
lemma cast_negOnePow (K : Type*) (n : ℤ) [Field K] : n.negOnePow = (-1 : K) ^ n

Proof state:
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ -1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case intro.inr
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
n : ℤ
inst✝ : Field K
⊢ ↑↑n.negOnePow = (-1) ^ n

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩

Result:
case intro.inl
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ ↑↑(2 * k).negOnePow = (-1) ^ (2 * k)

case intro.inr
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)

Proof state:
case intro.inl
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ ↑↑(2 * k).negOnePow = (-1) ^ (2 * k)

Tactic:
simp [zpow_mul, zpow_ofNat]

Result:
no goals

Proof state:
case intro.inr
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)

Tactic:
rw [zpow_add_one₀ (by norm_num), zpow_mul, zpow_ofNat]

Result:
case intro.inr
K : Type u_1
inst✝ : Field K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_last (n : ℕ) : cycleRange (last n) = finRotate (n + 1)

Proof state:
case H.h
n : ℕ
i : Fin (n + 1)
⊢ ↑((last n).cycleRange i) = ↑((finRotate (n + 1)) i)

Tactic:
rw [coe_cycleRange_of_le (le_last _), coe_finRotate]

Result:
no goals

Proof state:
n : ℕ
⊢ (last n).cycleRange = finRotate (n + 1)

Tactic:
ext i

Result:
case H.h
n : ℕ
i : Fin (n + 1)
⊢ ↑((last n).cycleRange i) = ↑((finRotate (n + 1)) i)
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_zero : rescale 0 = (C R).comp (constantCoeff R)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ rescale 0 = (C R).comp (constantCoeff R)

Tactic:
ext x n

Result:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff R n) ((rescale 0) x) = (coeff R n) (((C R).comp (constantCoeff R)) x)

Proof state:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff R n) ((rescale 0) x) = (coeff R n) (((C R).comp (constantCoeff R)) x)

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk,
  PowerSeries.coeff_mk _ _, coeff_C]

Result:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff R n) ({ toFun := fun f => mk fun n => 0 ^ n * (coeff R n) f, map_one' := ⋯, map_mul' := ⋯ } x) =
    if n = 0 then (constantCoeff R) x else 0

Proof state:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff R n) ({ toFun := fun f => mk fun n => 0 ^ n * (coeff R n) f, map_one' := ⋯, map_mul' := ⋯ } x) =
    if n = 0 then (constantCoeff R) x else 0

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Topology/Homotopy/Product.lean
theorem pi_proj (p : Path.Homotopic.Quotient as bs) : (pi fun i => proj i p) = p

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi fun i => proj i p) = p

Tactic:
induction p using Quotient.inductionOn

Result:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ (pi fun i => proj i ⟦a✝⟧) = ⟦a✝⟧

Proof state:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ (pi fun i => proj i ⟦a✝⟧) = ⟦a✝⟧

Tactic:
simp_rw [proj, ← Path.Homotopic.map_lift]

Result:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ (pi fun i => ⟦a✝.map ⋯⟧) = ⟦a✝⟧

Proof state:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ ⟦Path.pi fun i => a✝.map ⋯⟧ = ⟦a✝⟧

Tactic:
congr

Result:
no goals

Proof state:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ (pi fun i => ⟦a✝.map ⋯⟧) = ⟦a✝⟧

Tactic:
erw [pi_lift]

Result:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a✝ : Path as bs
⊢ ⟦Path.pi fun i => a✝.map ⋯⟧ = ⟦a✝⟧
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldr_eq_foldr_toList {s : RBNode.Stream α} : s.foldr f init = s.toList.foldr f init

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝ → α✝
init : α✝
s : RBNode.Stream α
⊢ foldr f s init = List.foldr f init s.toList

Tactic:
induction s <;> simp [*, RBNode.foldr_eq_foldr_toList]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsSeparable.iUnion {ι : Sort*} [Countable ι] {s : ι → Set α}
    (hs : ∀ i, IsSeparable (s i)) : IsSeparable (⋃ i, s i)

Proof state:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), (c i).Countable
h'c : ∀ (i : ι), s i ⊆ closure (c i)
⊢ IsSeparable (⋃ i, s i)

Tactic:
refine ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => ?_⟩

Result:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), (c i).Countable
h'c : ∀ (i : ι), s i ⊆ closure (c i)
i : ι
⊢ s i ⊆ closure (⋃ i, c i)

Proof state:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (⋃ i, s i)

Tactic:
choose c hc h'c using hs

Result:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), (c i).Countable
h'c : ∀ (i : ι), s i ⊆ closure (c i)
⊢ IsSeparable (⋃ i, s i)

Proof state:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), (c i).Countable
h'c : ∀ (i : ι), s i ⊆ closure (c i)
i : ι
⊢ s i ⊆ closure (⋃ i, c i)

Tactic:
exact (h'c i).trans (closure_mono (subset_iUnion _ i))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_alterKey (k k' : α) (f : Option (β k) → Option (β k))
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast? k' (alterKey k f l) =
      if h : k == k' then
        cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (getValueCast? k l))
      else
        getValueCast? k' l

Proof state:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
⊢ getValueCast? k (alterKey k f l) = cast ⋯ (f (getValueCast? k l))

Tactic:
simp only [Function.comp_apply, cast_eq]

Result:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
⊢ getValueCast? k (alterKey k f l) = f (getValueCast? k l)

Proof state:
case refl.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
heq : (k == k) = true
x✝ : Option (β k)
v✝ : β k
heq✝ : f (getValueCast? k l) = some v✝
⊢ getValueCast? k (insertEntry k v✝ l) = f (getValueCast? k l)

Tactic:
next hsome =>
rw [hsome, getValueCast?_insertEntry_self]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem absorbent_nhds_zero (hA : A ∈ 𝓝 (0 : E)) : Absorbent 𝕜 A :=
  absorbent_iff_inv_smul.2 fun x ↦ Filter.tendsto_inv₀_cobounded.smul tendsto_const_nhds <| by
    rwa [zero_smul]

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
⊢ A ∈ 𝓝 (0 • x)

Tactic:
rwa [zero_smul]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.add {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) :
    (T + S).IsSymmetric

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ inner ((T + S) x) y = inner x ((T + S) y)

Tactic:
rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
⊢ (T + S).IsSymmetric

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ inner ((T + S) x) y = inner x ((T + S) y)
-- Mathlib/Topology/Category/Stonean/Basic.lean
lemma Gleason (X : CompHaus.{u}) :
    Projective X ↔ ExtremallyDisconnected X

Proof state:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop

Tactic:
show ExtremallyDisconnected X.toStonean

Result:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toStonean.toTop

Proof state:
X : CompHaus
⊢ Projective X ↔ ExtremallyDisconnected ↑X.toTop

Tactic:
constructor

Result:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X

Proof state:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

Tactic:
intro h

Result:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop

Proof state:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : Stonean := CompHausLike.mk X.toTop ⋯
⊢ Projective X'.compHaus

Tactic:
apply Stonean.instProjectiveCompHausCompHaus

Result:
no goals

Proof state:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toStonean.toTop

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X

Tactic:
intro h

Result:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
⊢ Projective X

Proof state:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
⊢ Projective X

Tactic:
let X' : Stonean := ⟨X.toTop, inferInstance⟩

Result:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : Stonean := CompHausLike.mk X.toTop ⋯
⊢ Projective X

Proof state:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : Stonean := CompHausLike.mk X.toTop ⋯
⊢ Projective X

Tactic:
show Projective X'.compHaus

Result:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : Stonean := CompHausLike.mk X.toTop ⋯
⊢ Projective X'.compHaus
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem insertIdx_of_length_lt (l : List α) (x : α) (n : Nat) (h : l.length < n) :
    insertIdx n x l = l

Proof state:
case nil.zero
α : Type u
x : α
h : [].length < 0
⊢ insertIdx 0 x [] = []

Tactic:
simp at h

Result:
no goals

Proof state:
case nil.succ
α : Type u
x : α
n✝ : Nat
h : [].length < n✝ + 1
⊢ insertIdx (n✝ + 1) x [] = []

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
n✝ : Nat
h : (x :: l).length < n✝ + 1
⊢ insertIdx (n✝ + 1) x✝ (x :: l) = x :: l

Tactic:
simp only [Nat.succ_lt_succ_iff, length] at h

Result:
case cons.succ
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
n✝ : Nat
h : l.length < n✝
⊢ insertIdx (n✝ + 1) x✝ (x :: l) = x :: l

Proof state:
case cons
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
n : Nat
h : (x :: l).length < n
⊢ insertIdx n x✝ (x :: l) = x :: l

Tactic:
cases n

Result:
case cons.zero
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
h : (x :: l).length < 0
⊢ insertIdx 0 x✝ (x :: l) = x :: l

case cons.succ
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
n✝ : Nat
h : (x :: l).length < n✝ + 1
⊢ insertIdx (n✝ + 1) x✝ (x :: l) = x :: l

Proof state:
case cons.zero
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
h : (x :: l).length < 0
⊢ insertIdx 0 x✝ (x :: l) = x :: l

Tactic:
simp at h

Result:
no goals

Proof state:
case nil
α : Type u
x : α
n : Nat
h : [].length < n
⊢ insertIdx n x [] = []

Tactic:
cases n

Result:
case nil.zero
α : Type u
x : α
h : [].length < 0
⊢ insertIdx 0 x [] = []

case nil.succ
α : Type u
x : α
n✝ : Nat
h : [].length < n✝ + 1
⊢ insertIdx (n✝ + 1) x [] = []

Proof state:
case cons.succ
α : Type u
x✝ x : α
l : List α
ih : ∀ (n : Nat), l.length < n → insertIdx n x✝ l = l
n✝ : Nat
h : l.length < n✝
⊢ insertIdx (n✝ + 1) x✝ (x :: l) = x :: l

Tactic:
simpa using ih _ h

Result:
no goals
-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem identify_one (i : I) : ι' R A (DirectSum.lof R I A i 1) = 1

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((lof R I A i) 1) = 1

Tactic:
suffices ι' R A (DirectSum.lof R I A i 1) = mkAlgHom R A 1 by simpa

Result:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((lof R I A i) 1) = (mkAlgHom R A) 1

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
this : (ι' R A) ((lof R I A i) 1) = (mkAlgHom R A) 1
⊢ (ι' R A) ((lof R I A i) 1) = 1

Tactic:
simpa

Result:
no goals

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((lof R I A i) 1) = (mkAlgHom R A) 1

Tactic:
exact RingQuot.mkAlgHom_rel R <| rel_id R A (i := i)

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem closure_induced {f : α → β} {a : α} {s : Set α} :
    a ∈ @closure α (t.induced f) s ↔ f a ∈ closure (f '' s)

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
this : TopologicalSpace α := induced f t
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)

Tactic:
simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)

Tactic:
letI := t.induced f

Result:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
this : TopologicalSpace α := induced f t
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_congr_set (hu : s =ᶠ[𝓝 x] t) :
    LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g (s ∩ {x | (fun x => s x = t x) x}) x = LiftPropWithinAt P g (t ∩ {x | (fun x => s x = t x) x}) x

Tactic:
congr 1

Result:
case e_s
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ s ∩ {x | (fun x => s x = t x) x} = t ∩ {x | (fun x => s x = t x) x}

Proof state:
case e_s
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ s ∩ {x | (fun x => s x = t x) x} = t ∩ {x | (fun x => s x = t x) x}

Tactic:
aesop

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x

Tactic:
rw [← hG.liftPropWithinAt_inter (s := s) hu, ← hG.liftPropWithinAt_inter (s := t) hu,
  ← eq_iff_iff]

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g (s ∩ {x | (fun x => s x = t x) x}) x = LiftPropWithinAt P g (t ∩ {x | (fun x => s x = t x) x}) x
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.cellFrontier_subset_base_union_finite_closedCell [RelCWComplex C D]
    (n : ℕ) (i : cell C n) : ∃ I : Π m, Finset (cell C m), cellFrontier n i ⊆
    D ∪ ⋃ (m < n) (j ∈ I m), closedCell m j

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
rw [mapsTo'] at hI

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Proof state:
case intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
use I

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
exact hI

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ∃ I, cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
rcases mapsTo n i with ⟨I, hI⟩

Result:
case intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
/-- An open ball in a product space is a product of open balls. See also `ball_pi'`
for a version assuming `Nonempty β` instead of `0 < r`. -/
lemma ball_pi (x : ∀ b, π b) {r : ℝ} (hr : 0 < r) :
    ball x r = Set.pi univ fun b => ball (x b) r

Proof state:
case h
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 < r
p : (b : β) → π b
⊢ p ∈ ball x r ↔ p ∈ Set.univ.pi fun b => ball (x b) r

Tactic:
simp [dist_pi_lt_iff hr]

Result:
no goals

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 < r
⊢ ball x r = Set.univ.pi fun b => ball (x b) r

Tactic:
ext p

Result:
case h
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 < r
p : (b : β) → π b
⊢ p ∈ ball x r ↔ p ∈ Set.univ.pi fun b => ball (x b) r
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebraFin [NormOneClass A] :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1

Tactic:
cases n

Result:
case zero
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = 1

case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ = 1

Proof state:
case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ 1 ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖

Tactic:
refine le_of_eq_of_le ?_ <|
  ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1

Result:
case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ 1 = ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n✝.succ A) fun x => 1‖ / ∏ i : Fin n✝.succ, ‖1‖

Proof state:
case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ 1 = ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n✝.succ A) fun x => 1‖ / ∏ i : Fin n✝.succ, ‖1‖

Tactic:
simp

Result:
no goals

Proof state:
case zero
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖1‖ = 1

Tactic:
simp

Result:
no goals

Proof state:
case zero
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = 1

Tactic:
rw [norm_mkPiAlgebraFin_zero]

Result:
case zero
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖1‖ = 1

Proof state:
case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ = 1

Tactic:
refine le_antisymm norm_mkPiAlgebraFin_succ_le ?_

Result:
case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ 1 ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖