mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.rangeIcc g).support ⊆ f.support ∪ g.support

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
x✝ : i ∈ f.support
⊢ #(f i) = (fun i ↦ ↑(#(f i))) i (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ #f.pi = f.prod fun i ↦ ↑(#(f i))

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ x ∈ (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g) ↔ f ≤ x ∧ x ≤ g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ 2 * count b l

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length / 2 ≤ count b l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ 2 * count b l ≤ l.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ toDFinsupp (replicate n a) = DFinsupp.single a n

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ toDFinsupp {a} = DFinsupp.single a 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ DFinsupp.toMultiset.comp toDFinsupp = AddMonoidHom.id (Multiset α)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp.comp DFinsupp.toMultiset = AddMonoidHom.id (Π₀ (x : α), ℕ)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp s ≤ toDFinsupp t ↔ s ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → DecidableEq (α i)
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), IsBotZeroClass (α i)
inst✝¹ : (i : ι) → OrderBot (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f ≤ toMultiset g ↔ f ≤ g

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → DecidableEq (α i)
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), IsBotZeroClass (α i)
inst✝¹ : (i : ι) → OrderBot (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊓ g)) = Multiset.toDFinsupp (toMultiset f ∩ toMultiset g)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊔ g)) = Multiset.toDFinsupp (toMultiset f ∪ toMultiset g)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a : α
⊢ (mk a).out = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ mk (out ⟨s, h⟩) = ⟨s, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a b : Erased α
h : a.out = b.out
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ (map f a).out = f a.out

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1}, Functor.mapConst = Functor.map ∘ Function.const β

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Erased α), id <$> x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : Erased α) (y : Erased β), x <* y = Function.const β <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : Erased α) (y : Erased β), x *> y = Function.const α id <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (g : α → β) (x : Erased α), pure g <*> x = g <$> x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : α → β) (x : Erased α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : Erased (α → β)) (x : Erased α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      f <*> x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : α) (f : α → Erased β), pure x >>= f = f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (x : Erased α) (f : α → Erased β) (g : β → Erased γ), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ (∑ a ∈ s, f a).toNat = ∑ a ∈ s, (f a).toNat

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hlt : ∀ i ∈ s, f i < g i
⊢ ∑ i ∈ s, f i < ∑ i ∈ s, g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : Finset α
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur s q = q.blur' h

Tactic:
by

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + ↑prec - 1 ≤ ↑emax

Tactic:
by

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ emin = max (emin + ↑(Nat.size 0) - ↑prec) emin

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ a ∈ q, ∀ b ∈ q, f a = f b
a : α
aq : a ∈ q
⊢ q.liftOn f h = f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
this : ∀ (k : Fin (n + 1)), f k < x
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
q : Semiquot α
⊢ ∀ (a : α), a ∈ id <$> q ↔ a ∈ q

Tactic:
by

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
n d : ℕ+
⊢ Float × Bool

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β : Type u_3
x : α
f : α → Semiquot β
⊢ ∀ (a : β), a ∈ pure x >>= f ↔ a ∈ f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ a ∈ s >>= fun x ↦ f x >>= g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β : Type u_3
f : α → β
s : Semiquot α
⊢ ∀ (a : β),
    (a ∈ do
        let y ← s
        pure (f y)) ↔
      a ∈ f <$> s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
⊢ q.get p ∈ q

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ a ∈ pure (q.get p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : ValidFinite e m
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ ValidFinite e m'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ t ≤ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
⊢ IsMaxChain (fun x1 x2 ↦ x1 ≤ x2) (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m m' : ℕ
v : ValidFinite e m'.succ
h : m = m'.succ
ss : m'.size = m.size
⊢ ValidFinite e m'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: n k : ℕ
h : k = 2 ^ n
a b c : Fin k
⊢ a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: k : ℕ
a b : Fin k
⊢ a ^^^ b = b ^^^ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: k : ℕ
inst✝ : NeZero k
a : Fin k
⊢ a ^^^ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: k : ℕ
inst✝ : NeZero k
a : Fin k
⊢ a ^^^ 0 = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
⊢ m ≤ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
⊢ P (f ∘ ⇑(sort f))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m ↪ Fin n
⊢ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
b : Fin n
hb : b ∉ Set.range f
⊢ m < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m n : ℕ
f : Fin m → Fin n
hf : Function.Surjective f
⊢ n ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Pigeonhole

Goal state before:
pp: m : ℕ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Fin m → α
⊢ Fintype.card ↑(Set.range f) ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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 π')) σ')
⊢ Continuous fun x ↦ ⟨σ' none x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
⊢ init (snoc x ha) = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
i : Fin n
⊢ (snoc x ha) i.castSucc = x i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬a ∈ range ⇑x
⊢ (snoc x ha) (last n) = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
e : Fin 2 ↪ α
⊢ (e 0, e 1) ∈ {(a, b) | a ≠ b}

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ i = j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
e : Fin 2 ↪ α
⊢ (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) =
    e

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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
⊢ Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take 0 ⋯ v = fun i ↦ i.elim0

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take 1 ⋯ v = fun i ↦ v (castLE ⋯ i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take n ⋯ v = v

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
⊢ take (m * n') ⋯ («repeat» n a) = «repeat» m a

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ i = 0

Tactic:
by

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

Goal state before:
pp: case succ.cast
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)
a✝ : take (m + 1).succ h v i.succ = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.succ
⊢ take (m + 1).succ h v i.castSucc = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.castSucc

Tactic:
| cast i _ =>

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ castLE h j ≠ castLE h i

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
⊢ (curry f).uncurry = f

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ castLE h j ≠ i

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
x : ↑T'.toTop
hx : (⇑(ConcreteCategory.hom (snd S' ℕ∪{∞})) ∘ ⇑(ConcreteCategory.hom π')) x = ∞
⊢ x ∈ ⇑(ConcreteCategory.hom (π' ≫ snd S' ℕ∪{∞})) ⁻¹' {∞}

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
⊢ take m h (update v i x) = take m h v

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
⊢ Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ List.idxOf x xs < xs.length

Tactic:
by

Goal state after: