awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : applyId (xs.zip ys) y ∉ ys
hy : applyId (xs.zip ys) y ∈ ys
⊢ x = y

Tactic:
contradiction
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
neg : ∀ (h : x = applyId (xs.zip ys) y) (hx : x ∉ xs) (hy : y ∉ xs), y ∉ xs
neg₁ : x ∉ xs
⊢ x = y

Tactic:
rwa [List.applyId_eq_self, List.applyId_eq_self] at h

Premises used: Plausible.InjectiveFunction.List.applyId_eq_self
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ y ∉ xs

Tactic:
assumption
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x ∉ xs

Tactic:
assumption
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
x : ℕ
n : ℕ := x
h : 0 < n
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α_1 : Type u
β : Type v
α : Type
inst : DecidableEq α
xs : List ((_ : α) × α)
h₀_1 : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
h₁_1 : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : ys'.Nodup
h₃ : xs'.length ≤ ys'.length
h₄ : ys'.length ≤ xs'.length
⊢ map (Sigma.fst (β := fun (x : α) ↦ α)) (map Prod.toSigma (xs'.zip ys')) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (map Prod.toSigma (xs'.zip ys'))

Tactic:
simp only [comp_def, List.map_fst_zip, List.map_snd_zip, *, Prod.fst_toSigma,
          Prod.snd_toSigma, List.map_map]

Premises used: List.map_map, List.map_fst_zip, Prod.fst_toSigma, Function.comp_def, List.map_snd_zip, Prod.snd_toSigma
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α_1 : Type u
β : Type v
α : Type
inst : DecidableEq α
xs : List ((_ : α) × α)
h₀_1 : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
h₁_1 : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : ys'.Nodup
h₃ : xs'.length ≤ ys'.length
h₄ : ys'.length ≤ xs'.length
⊢ Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (map Prod.toSigma (xs'.zip ys')))

Tactic:
simp only [comp_def, List.map_snd_zip, *, Prod.snd_toSigma, List.map_map]

Premises used: List.map_map, Function.comp_def, List.map_snd_zip, Prod.snd_toSigma
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
xs ys : List α
h : xs ~ ys
h' : ys.Nodup
h₀ : xs.length ≤ ys.length
h₁ : ys.length ≤ xs.length
⊢ map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs.zip ys)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs.zip ys))

Tactic:
simp only [List.toFinmap', comp_def, List.map_fst_zip, List.map_snd_zip, *,
        List.map_map]

Premises used: List.map_map, List.map_fst_zip, Plausible.TotalFunction.List.toFinmap', Function.comp_def, List.map_snd_zip
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
xs ys : List α
h : xs ~ ys
h' : ys.Nodup
h₀ : xs.length ≤ ys.length
h₁ : ys.length ≤ xs.length
⊢ Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs.zip ys)))

Tactic:
simp only [List.toFinmap', comp_def, List.map_snd_zip, *, List.map_map]

Premises used: List.map_map, Plausible.TotalFunction.List.toFinmap', Function.comp_def, List.map_snd_zip
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
f : InjectiveFunction α
obtain :
  ∀ (xs : List ((_ : α) × α))
    (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)), Injective (mapToSelf xs hperm hnodup).apply
⊢ Injective f.apply

Tactic:
obtain ⟨xs, hperm, hnodup⟩ := f
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
generalize :
  ∀ (xs₀ : List α) (h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀), Injective (mapToSelf xs hperm hnodup).apply
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
generalize h₀ : List.map Sigma.fst xs = xs₀

Premises used: List.map, Sigma.fst
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
generalize :
  ∀ (xs₁ : List α) (h₁ : map (id (Sigma.snd (β := fun (x : α) ↦ α))) xs = xs₁),
    Injective (mapToSelf xs hperm hnodup).apply
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁

Premises used: List.map, id, Sigma.snd
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
rw :
  xs =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs))
⊢ xs = List.toFinmap' (xs₀.zip xs₁)

Tactic:
rw [← h₀, ← h₁, List.toFinmap']

Premises used: Plausible.TotalFunction.List.toFinmap'
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
⊢ Eq.{u + 1} (α := List ((_ : α) × α)) []
    (map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      (zip (map (α := (_ : α) × α) (Sigma.fst (β := fun (x : α) ↦ α)) [])
        (map (α := (_ : α) × α) (Sigma.snd (β := fun (x : α) ↦ α)) [])))

Tactic:
simp only [List.zip_nil_right, List.map_nil]

Premises used: List.zip_nil_right, List.map_nil
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))
cons :
  xs_tl =
    map (fun (x : α × α) ↦ Sigma.mk (β := fun (x : α) ↦ α) x.1 x.2)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))
⊢ xs_hd :: xs_tl =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) (xs_hd :: xs_tl)).zip
        (map (Sigma.snd (β := fun (x : α) ↦ α)) (xs_hd :: xs_tl)))

Tactic:
simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]

Premises used: Sigma.eta, List.map, List.cons_inj_right, List.zip_cons_cons
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))
⊢ xs_tl =
    map (fun (x : α × α) ↦ Sigma.mk (β := fun (x : α) ↦ α) x.1 x.2)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))

Tactic:
xs_ih
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))
⊢ xs_tl =
    map (fun (x : α × α) ↦ Sigma.mk (β := fun (x : α) ↦ α) x.1 x.2)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))

Tactic:
exact xs_ih
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
nil :
  Eq.{u + 1} (α := List ((_ : α) × α)) []
    (map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      (zip (map (α := (_ : α) × α) (Sigma.fst (β := fun (x : α) ↦ α)) [])
        (map (α := (_ : α) × α) (Sigma.snd (β := fun (x : α) ↦ α)) [])))
cons :
  ∀ (xs_hd : (_ : α) × α) (xs_tl : List ((_ : α) × α))
    (xs_ih :
      xs_tl =
        map
          (fun (x : α × α) ↦
            match (motive := α × α → (_ : α) × α) x with
            | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
          ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs_tl).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs_tl))),
    xs_hd :: xs_tl =
      map
        (fun (x : α × α) ↦
          match (motive := α × α → (_ : α) × α) x with
          | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
        ((map (Sigma.fst (β := fun (x : α) ↦ α)) (xs_hd :: xs_tl)).zip
          (map (Sigma.snd (β := fun (x : α) ↦ α)) (xs_hd :: xs_tl)))
⊢ xs =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs))

Tactic:
induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih

Premises used: Sigma.eta, List.map, List.cons_inj_right, List.cons, List.zip_nil_right, List.map_nil, List.nil, List.zip_cons_cons
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
⊢ xs = List.toFinmap' (xs₀.zip xs₁)

Tactic:
have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) := by
    rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
    induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
revert :
  ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)), Injective (mapToSelf xs hperm hnodup).apply
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
revert hperm hnodup
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
rw :
  ∀
    (hperm :
      map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
        map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
⊢ ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)), Injective (mapToSelf xs hperm hnodup).apply

Tactic:
rw [hxs]
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ : xs₀.Nodup
h₃ : xs₀ ~ xs₁
⊢ Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply

Tactic:
apply InjectiveFunction.applyId_injective

Premises used: Plausible.InjectiveFunction.applyId_injective
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ : (map (Sigma.fst (β := fun (x : α) ↦ α)) xs).Nodup
h₃ : (map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))).Nodup
h₄ h₅ h₆ h₇ : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
⊢ xs₀.Nodup

Tactic:
rwa [← h₀, hxs, hperm.nodup_iff]

Premises used: List.Perm.nodup_iff
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm :
  map (Sigma.fst (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)) ~
    map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁))
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))
h₂ :
  ∀ (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
h₃ :
  ∀ (hperm : xs₀ ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
h₄ h₅ h₆ h₇ :
  ∀ (hperm : xs₀ ~ xs₁)
    (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) (List.toFinmap' (xs₀.zip xs₁)))), xs₀ ~ xs₁
⊢ xs₀ ~ xs₁

Tactic:
rwa [← hxs, h₀, h₁] at hperm
-- Module: Mathlib.Testing.Plausible.Sampleable
Goal:
⊢ SampleableExt Rat

Tactic:
infer_instance
-- Module: Mathlib.Testing.Plausible.Sampleable
Goal:
⊢ SampleableExt ℕ+

Tactic:
infer_instance
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
simp_rw :
  Eq (α := Prop) (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x))
    (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x))
⊢ AlexandrovDiscrete α = ∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x)

Tactic:
simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]

Premises used: Function.Surjective.forall, alexandrovDiscrete_iff, compl_surjective, Set.compl_sUnion, Function.Surjective.image_surjective, isOpen_compl_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
tactic : ∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x)
| AlexandrovDiscrete α

Tactic:
tactic =>
    simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]

Premises used: Function.Surjective.forall, alexandrovDiscrete_iff, compl_surjective, Set.compl_sUnion, Function.Surjective.image_surjective, isOpen_compl_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
conv_lhs : AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
conv_lhs₁ :
  (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsClosed[inst] x_1) → IsClosed[inst] (⋃₀ x)) ↔
    ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)
⊢ AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed[inst] s) → IsClosed[inst] (⋃₀ S)

Tactic:
conv_lhs => tactic =>
    simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]

Premises used: Function.Surjective.forall, alexandrovDiscrete_iff, compl_surjective, Set.compl_sUnion, Function.Surjective.image_surjective, isOpen_compl_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : IndiscreteTopology α
⊢ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen[inst] s) → IsOpen[inst] (⋂₀ S)

Tactic:
grind [isOpen_iff]

Premises used: IndiscreteTopology.isOpen_iff
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
⊢ (∀ s ∈ S, IsOpen[inst] s) → IsOpen[inst] (⋂₀ S)

Tactic:
AlexandrovDiscrete.isOpen_sInter _

Premises used: AlexandrovDiscrete.isOpen_sInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : ι → Set α
hf : ∀ (i : ι), IsOpen[inst] (f i)
⊢ IsOpen[inst] (⋂ (i : ι), f i)

Tactic:
isOpen_sInter <| forall_mem_range.2 hf

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, isOpen_sInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsOpen[inst] (f i j)
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
isOpen_iInter fun _ ↦ isOpen_iInter <| hf _

Premises used: isOpen_iInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
hS : ∀ s ∈ S, IsClosed[inst] s
⊢ IsClosed[inst] (⋃₀ S)

Tactic:
alexandrovDiscrete_iff_isClosed.mp inferInstance S hS

Premises used: alexandrovDiscrete_iff_isClosed, inferInstance, Iff.mp
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : ι → Set α
hf : ∀ (i : ι), IsClosed[inst] (f i)
⊢ IsClosed[inst] (⋃ (i : ι), f i)

Tactic:
isClosed_sUnion <| forall_mem_range.2 hf

Premises used: Iff.mpr, Set.forall_mem_range, iSup, isClosed_sUnion, Set.iUnion
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsClosed[inst] (f i j)
⊢ IsClosed[inst] (⋃ (i : ι), ⋃ (j : κ i), f i j)

Tactic:
isClosed_iUnion fun _ ↦ isClosed_iUnion <| hf _

Premises used: isClosed_iUnion
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
hS : ∀ s ∈ S, IsClopen s
⊢ IsClopen (⋂₀ S)

Tactic:
⟨isClosed_sInter fun s hs ↦ (hS s hs).1, isOpen_sInter fun s hs ↦ (hS s hs).2⟩

Premises used: isOpen_sInter, And.right, And.left, And.intro, isClosed_sInter, IsClopen
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : ι → Set α
hf : ∀ (i : ι), IsClopen (f i)
⊢ IsClopen.{u_3} (X := α) (⋂ (i : ι), f i)

Tactic:
⟨isClosed_iInter fun i ↦ (hf i).1, isOpen_iInter fun i ↦ (hf i).2⟩

Premises used: And.right, And.left, isOpen_iInter, And.intro, IsClopen, isClosed_iInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)
⊢ IsClopen.{u_3} (X := α) (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
isClopen_iInter fun _ ↦ isClopen_iInter <| hf _

Premises used: isClopen_iInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
hS : ∀ s ∈ S, IsClopen s
⊢ IsClopen (⋃₀ S)

Tactic:
⟨isClosed_sUnion fun s hs ↦ (hS s hs).1, isOpen_sUnion fun s hs ↦ (hS s hs).2⟩

Premises used: isClosed_sUnion, And.right, And.left, And.intro, IsClopen, isOpen_sUnion
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : ι → Set α
hf : ∀ (i : ι), IsClopen (f i)
⊢ IsClopen.{u_3} (X := α) (⋃ (i : ι), f i)

Tactic:
⟨isClosed_iUnion fun i ↦ (hf i).1, isOpen_iUnion fun i ↦ (hf i).2⟩

Premises used: isClosed_iUnion, isOpen_iUnion, And.right, And.left, And.intro, IsClopen
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)
⊢ IsClopen.{u_3} (X := α) (⋃ (i : ι), ⋃ (j : κ i), f i j)

Tactic:
isClopen_iUnion fun _ ↦ isClopen_iUnion <| hf _

Premises used: isClopen_iUnion
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : ι → Set α
⊢ Eq.{u_3 + 1} (α := Set α) (interior (⋂ (i : ι), f i)) (⋂ (i : ι), interior (f i))

Tactic:
(interior_maximal (iInter_mono fun _ ↦ interior_subset) <| isOpen_iInter fun _ ↦
    isOpen_interior).antisymm' <| subset_iInter fun _ ↦ interior_mono <| iInter_subset _ _

Premises used: interior_subset, interior_mono, isOpen_interior, Set.subset_iInter, interior_maximal, isOpen_iInter, Set.iInter_subset, Set.iInter_mono, HasSubset.Subset.antisymm'
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
simp_rw : Eq.{u_3 + 1} (α := Set α) (interior (⋂ i ∈ S, i)) (⋂ s ∈ S, interior s)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
simp_rw [sInter_eq_biInter, interior_iInter]

Premises used: Set.sInter_eq_biInter, interior_iInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
f : ι → Set α
⊢ Eq.{u_3 + 1} (α := Set α) (closure[inst] (⋃ (i : ι), f i))ᶜ (⋃ (i : ι), closure[inst] (f i))ᶜ

Tactic:
simpa only [← interior_compl, compl_iUnion] using interior_iInter fun i ↦ (f i)ᶜ

Premises used: Compl.compl, Set.compl_iUnion, interior_iInter, interior_compl