mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_5
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi (cover ({ hom := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ } } ≫ π'))

Tactic:
·

Goal state after:
case refine_5
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi (cover ({ hom := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ } } ≫ π'))
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
⊢ i = j

pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

Tactic:
·

Goal state after:
case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
⊢ i = j
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : j = 0
⊢ i = j

pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

Tactic:
·

Goal state after:
case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : j = 0
⊢ i = j
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

Tactic:
·

Goal state after:
case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

Tactic:
·

Goal state after:
case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
hj : j = 0
⊢ 1 = j

pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ 1 = j

Tactic:
·

Goal state after:
case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
hj : j = 0
⊢ 1 = j
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ 1 = j

Tactic:
·

Goal state after:
case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ 1 = j
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

pp: case neg
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
·

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case pos
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

pp: case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

Tactic:
·

Goal state after:
case pos
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

Tactic:
·

Goal state after:
case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case succ
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
i : Fin (m + 1).succ
⊢ take (m + 1).succ h v i = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i

Tactic:
| succ m _ =>

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

pp: case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
·

Goal state after:
case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
·

Goal state after:
case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty = congr x✝ inst✝ ⋯ empty

pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr x✝ inst✝ ⋯ empty

Tactic:
·

Goal state after:
case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty = congr x✝ inst✝ ⋯ empty
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr x✝ inst✝ ⋯ empty

Tactic:
·

Goal state after:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr x✝ inst✝ ⋯ empty
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
·

Goal state after:
case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
·

Goal state after:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

pp: case neg
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ¬↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
·

Goal state after:
case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case neg
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ¬↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
·

Goal state after:
case neg
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ¬↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_2
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ card α = 0

pp: case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ equiv ≍ Equiv.equivOfIsEmpty α (Fin 0)

pp: case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
·

Goal state after:
case e_2
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ card α = 0
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ equiv ≍ Equiv.equivOfIsEmpty α (Fin 0)

pp: case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
·

Goal state after:
case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ equiv ≍ Equiv.equivOfIsEmpty α (Fin 0)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
·

Goal state after:
case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_2
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ card α = 1

pp: case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ equiv ≍ Equiv.ofUnique α (Fin 1)

pp: case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
·

Goal state after:
case e_2
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ card α = 1
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ equiv ≍ Equiv.ofUnique α (Fin 1)

pp: case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
·

Goal state after:
case e_3
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ equiv ≍ Equiv.ofUnique α (Fin 1)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
·

Goal state after:
case e_4
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case none
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
h : g a = none
⊢ lookmap f (a :: l) = lookmap g (a :: l)

pp: case some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
·

Goal state after:
case none
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
h : g a = none
⊢ lookmap f (a :: l) = lookmap g (a :: l)
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
·

Goal state after:
case some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

pp: case some
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
·

Goal state after:
case none
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)