harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_one_left (n : Nat) : gcd 1 n = 1

Proof state:
n : Nat
⊢ gcd 1 n = 1

Tactic:
rw [gcd_succ, mod_one]

Result:
n : Nat
⊢ gcd 0 (succ 0) = 1

Proof state:
n : Nat
⊢ gcd 0 (succ 0) = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
    {xs : List α} → xs.max? = some a → a ∈ xs
  | nil => by simp
  | cons x xs => by
    rw [max?]; rintro ⟨⟩
    induction xs generalizing x with simp at *
    | cons y xs ih =>
      rcases ih (max x y) with h | h <;> simp [h]
      simp [← or_assoc, min_eq_or x y]

Proof state:
α : Type u_1
a : α
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
⊢ [].max? = some a → a ∈ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
x : α
xs : List α
⊢ some (foldl max x xs) = some a → a ∈ x :: xs

Tactic:
rintro ⟨⟩

Result:
case refl
α : Type u_1
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
x : α
xs : List α
⊢ foldl max x xs ∈ x :: xs

Proof state:
case refl
α : Type u_1
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
x : α
xs : List α
⊢ foldl max x xs ∈ x :: xs

Tactic:
induction xs generalizing x with simp at *
| cons y xs ih =>
  rcases ih (max x y) with h | h <;> simp [h]
  simp [← or_assoc, min_eq_or x y]

Result:
no goals

Proof state:
case refl.cons
α : Type u_1
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
y : α
xs : List α
x : α
ih : ∀ (x : α), foldl max x xs = x ∨ foldl max x xs ∈ xs
⊢ foldl max (max x y) xs = x ∨ foldl max (max x y) xs = y ∨ foldl max (max x y) xs ∈ xs

Tactic:
rcases ih (max x y) with h | h <;> simp [h]

Result:
case refl.cons.inl
α : Type u_1
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
y : α
xs : List α
x : α
ih : ∀ (x : α), foldl max x xs = x ∨ foldl max x xs ∈ xs
h : foldl max (max x y) xs = max x y
⊢ max x y = x ∨ max x y = y ∨ max x y ∈ xs

Proof state:
case refl.cons.inl
α : Type u_1
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
y : α
xs : List α
x : α
ih : ∀ (x : α), foldl max x xs = x ∨ foldl max x xs ∈ xs
h : foldl max (max x y) xs = max x y
⊢ max x y = x ∨ max x y = y ∨ max x y ∈ xs

Tactic:
simp [← or_assoc, min_eq_or x y]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
x : α
xs : List α
⊢ (x :: xs).max? = some a → a ∈ x :: xs

Tactic:
rw [max?]

Result:
α : Type u_1
a : α
inst✝ : Max α
min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
x : α
xs : List α
⊢ some (foldl max x xs) = some a → a ∈ x :: xs
-- Mathlib/Order/WellFounded.lean
theorem wellFounded_iff_has_min {r : α → α → Prop} :
    WellFounded r ↔ ∀ s : Set α, s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m

Proof state:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
⊢ Acc r x

Tactic:
by_contra hx

Result:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
⊢ False

Proof state:
α : Type u_1
r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m

Tactic:
refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩

Result:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
⊢ Acc r x

Proof state:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
⊢ False

Tactic:
obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩

Result:
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m
⊢ False

Proof state:
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False

Tactic:
exact hm' y hy' hy

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m
⊢ False

Tactic:
refine hm ⟨_, fun y hy => ?_⟩

Result:
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m
y : α
hy : r y m
⊢ Acc r y

Proof state:
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m
y : α
hy : r y m
⊢ Acc r y

Tactic:
by_contra hy'

Result:
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False

Proof state:
⊢ ∀ (b : Bool), (!b) = b ↔ False

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_map_left (l₁ : Array α) (l₂ : Array β) (f : α → α') (g : α' → β → γ) :
    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
f : α → α'
g : α' → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith g (map f { toList := toList✝¹ }) { toList := toList✝ } =
    zipWith (fun a b => g (f a) b) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWith_map_left]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
l₂ : Array β
f : α → α'
g : α' → β → γ
toList✝ : List α
⊢ zipWith g (map f { toList := toList✝ }) l₂ = zipWith (fun a b => g (f a) b) { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
f : α → α'
g : α' → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith g (map f { toList := toList✝¹ }) { toList := toList✝ } =
    zipWith (fun a b => g (f a) b) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
l₁ : Array α
l₂ : Array β
f : α → α'
g : α' → β → γ
⊢ zipWith g (map f l₁) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
l₂ : Array β
f : α → α'
g : α' → β → γ
toList✝ : List α
⊢ zipWith g (map f { toList := toList✝ }) l₂ = zipWith (fun a b => g (f a) b) { toList := toList✝ } l₂
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma isBasis_loops_iff : M.IsBasis I M.loops ↔ I = ∅ :=
  ⟨fun h ↦ h.indep.eq_empty_of_subset_loops h.subset,
    by simp +contextual [M.empty_indep.isBasis_closure]⟩

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ I = ∅ → M.IsBasis I M.loops

Tactic:
simp +contextual [M.empty_indep.isBasis_closure]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem exp_mem_exp [RCLike 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A)
    {z : 𝕜} (hz : z ∈ spectrum 𝕜 a) : exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
⊢ ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b

Tactic:
simpa only [mul_smul_comm, pow_succ'] using hb.tsum_mul_left (a - ↑ₐ z)

Result:
no goals
-- Mathlib/Topology/DiscreteSubset.lean
lemma mem_codiscrete {S : Set X} :
    S ∈ codiscrete X ↔ ∀ x, Disjoint (𝓝[≠] x) (𝓟 Sᶜ)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 Sᶜ)

Tactic:
simp [codiscrete, mem_codiscreteWithin, compl_eq_univ_diff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
    (as ++ bs)[i] = as[i]

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

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

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

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

Tactic:
conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]

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

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

Tactic:
rwa [← length_toList, toList_append] at h

Result:
no goals

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

Tactic:
rw [toList_append]

Result:
no goals

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

Tactic:
simp only [← getElem_toList]

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

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

Tactic:
apply List.get_of_eq

Result:
case h
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
hlt : i < as.size
h' : i < (as.toList ++ bs.toList).length
⊢ (as ++ bs).toList = as.toList ++ bs.toList
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma countableOrCountablyGenerated_prod_left_swap [h : CountableOrCountablyGenerated (α × β) γ] :
    CountableOrCountablyGenerated (β × α) γ

Proof state:
case mk.inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
exact ⟨Or.inr h⟩

Result:
no goals

Proof state:
case mk.inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
refine ⟨Or.inl countable_prod_swap⟩

Result:
no goals

Proof state:
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
rcases h with (h | h)

Result:
case mk.inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated (β × α) γ

case mk.inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_add_one (s : ℂ) (h2 : s ≠ 0) : Gamma (s + 1) = s * Gamma s

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
have t1 : -s.re < n := by simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)

Result:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ Gamma (s + 1) = s * Gamma s

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ -(s.re + 1) < ↑n

Tactic:
linarith

Result:
no goals

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ -s.re < ↑n

Tactic:
simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)

Result:
no goals

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
rw [Gamma_eq_GammaAux s n t1, Gamma_eq_GammaAux (s + 1) n t2, GammaAux_recurrence1 s n t1]

Result:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ -(s + 1).re < ↑n

Tactic:
rw [add_re, one_re]

Result:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ -(s.re + 1) < ↑n

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
have t2 : -(s + 1).re < n := by rw [add_re, one_re]; linarith

Result:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ Gamma (s + 1) = s * Gamma s

Proof state:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)

Tactic:
field_simp

Result:
no goals

Proof state:
s : ℂ
h2 : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
let n := ⌊1 - s.re⌋₊

Result:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ Gamma (s + 1) = s * Gamma s
-- Mathlib/Topology/Maps/Proper/CompactlyGenerated.lean
/-- Version of `isProperMap_iff_isCompact_preimage` in terms of `cocompact`.

There was an older version of this theorem which was changed to this one to make use
of the `CompactlyGeneratedSpace` typeclass. (since 2024-11-10) -/
lemma isProperMap_iff_tendsto_cocompact :
    IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ
⊢ IsCompact (f ⁻¹' K)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)

Tactic:
simp_rw [isProperMap_iff_isCompact_preimage,
  hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set, preimage_compl]

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X

Tactic:
refine and_congr_right fun f_cont ↦
  ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyGeneratedSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ
⊢ IsCompact (f ⁻¹' K)

Tactic:
exact hK'.of_isClosed_subset (hK.isClosed.preimage f_cont)
  (compl_le_compl_iff_le.mp hK'y)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/MinMax.lean
theorem max_comm (a b : Nat) : max a b = max b a

Proof state:
a b : Nat
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Tactic:
by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]

Result:
case pos
a b : Nat
h₁ : a ≤ b
h₂ : b ≤ a
⊢ b = a

case neg
a b : Nat
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ a = b

Proof state:
a b : Nat
⊢ max a b = max b a

Tactic:
simp only [Nat.max_def]

Result:
a b : Nat
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Proof state:
case neg
a b : Nat
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ a = b

Tactic:
cases not_or_intro h₁ h₂ <| Nat.le_total ..

Result:
no goals

Proof state:
case pos
a b : Nat
h₁ : a ≤ b
h₂ : b ≤ a
⊢ b = a

Tactic:
exact Nat.le_antisymm h₂ h₁

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem isOpenEmbedding_obj_top {X : TopCat} (U : Opens X) :
    U.isOpenEmbedding.isOpenMap.functor.obj ⊤ = U

Proof state:
case h
X : TopCat
U : Opens ↑X
⊢ ↑(⋯.functor.obj ⊤) = ↑U

Tactic:
exact Set.image_univ.trans Subtype.range_coe

Result:
no goals

Proof state:
X : TopCat
U : Opens ↑X
⊢ ⋯.functor.obj ⊤ = U

Tactic:
ext1

Result:
case h
X : TopCat
U : Opens ↑X
⊢ ↑(⋯.functor.obj ⊤) = ↑U
-- Mathlib/Order/Filter/Prod.lean
theorem map_snd_prod (f : Filter α) (g : Filter β) [NeBot f] : map Prod.snd (f ×ˢ g) = g

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map (Prod.snd ∘ fun p => (p.2, p.1)) (g ×ˢ f) = g

Tactic:
apply map_fst_prod

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map Prod.snd (f ×ˢ g) = g

Tactic:
rw [prod_comm, map_map]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map (Prod.snd ∘ fun p => (p.2, p.1)) (g ×ˢ f) = g
-- Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
theorem RingHom.IsIntegralElem.sub {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) :
    f.IsIntegralElem (x - y)

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
⊢ f.IsIntegralElem (x - y)

Tactic:
simpa only [sub_eq_add_neg] using hx.add f (hy.neg f)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f (i - 1)

Proof state:
case pos.isTrue.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : i - 1 = k
h✝¹ : k < j
h✝ : i = k
⊢ f l[k] = f l[k]

case pos.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : i - 1 = k
h✝¹ : k < j
h✝ : ¬i = k
⊢ l[k] = f l[k]

case pos.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : i - 1 = k
h✝¹ : ¬k < j
h✝ : i = k + 1
⊢ f l[k + 1] = f l[k + 1]

case pos.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : i - 1 = k
h✝¹ : ¬k < j
h✝ : ¬i = k + 1
⊢ l[k + 1] = f l[k + 1]

case neg.isTrue.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : k < j
h✝ : i = k
⊢ f l[k] = l[k]

case neg.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : k < j
h✝ : ¬i = k
⊢ l[k] = l[k]

case neg.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : ¬k < j
h✝ : i = k + 1
⊢ f l[k + 1] = l[k + 1]

case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : ¬k < j
h✝ : ¬i = k + 1
⊢ l[k + 1] = l[k + 1]

Tactic:
all_goals (first | rfl | omega)

Result:
no goals

Proof state:
case neg.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : ¬k < j
h✝ : i = k + 1
⊢ f l[k + 1] = l[k + 1]

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
protected lemma disjoint_iff {f g : Filter α} : Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t

Proof state:
α : Type u
f g : Filter α
⊢ Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t

Tactic:
simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff, inf_eq_inter, bot_eq_empty,
  @eq_comm _ ∅]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem one_lt_card : 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Proof state:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
exact card_le_one

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
s : Finset α
⊢ ¬1 < #s ↔ ¬∃ a ∈ s, ∃ b ∈ s, a ≠ b

Proof state:
α : Type u_1
s : Finset α
⊢ ¬1 < #s ↔ ¬∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
push_neg

Result:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_Iio : #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

Result:
no goals