harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
`f` is a monotone function on `D`. -/
lemma monotoneOn_of_hasDerivWithinAt_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
    (hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x) : MonotoneOn f D :=
  monotoneOn_of_deriv_nonneg hD hf (fun _ hx ↦ (hf' _ hx).differentiableWithinAt) fun x hx ↦ by
    rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ deriv f x

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Result:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x

Tactic:
exact hf'₀ _ hx

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
lemma power_le_aleph0 {a b : Cardinal.{u}} (ha : a ≤ ℵ₀) (hb : b < ℵ₀) : a ^ b ≤ ℵ₀

Proof state:
case intro
a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ a ^ ↑b ≤ ℵ₀

Tactic:
simpa [ha] using power_nat_le_max (c := a)

Result:
no goals

Proof state:
a b : Cardinal.{u}
ha : a ≤ ℵ₀
hb : b < ℵ₀
⊢ a ^ b ≤ ℵ₀

Tactic:
lift b to ℕ using hb

Result:
case intro
a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ a ^ ↑b ≤ ℵ₀
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l : Vector α n) (H) :
    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h))

Proof state:
α : Type u_1
n : Nat
p q : α → Prop
f : ∀ (a : α), p a → q a
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) l H = l.attachWith q ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p q : α → Prop
f : ∀ (a : α), p a → q a
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) { toArray := toArray✝, size_toArray := size_toArray✝ } H =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith q ⋯

Proof state:
case mk
α : Type u_1
n : Nat
p q : α → Prop
f : ∀ (a : α), p a → q a
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) { toArray := toArray✝, size_toArray := size_toArray✝ } H =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith q ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem traverse_eq_map_id {α β} (f : α → β) :
    ∀ x : Vector α n, x.traverse ((pure : _ → Id _) ∘ f) = (pure : _ → Id _) (map f x)

Proof state:
n : ℕ
α β : Type u_6
f : α → β
⊢ ∀ (x : Vector α n), Vector.traverse (pure ∘ f) x = pure (map f x)

Tactic:
rintro ⟨x, rfl⟩

Result:
case mk
α β : Type u_6
f : α → β
x : List α
⊢ Vector.traverse (pure ∘ f) ⟨x, ⋯⟩ = pure (map f ⟨x, ⋯⟩)

Proof state:
case mk
α β : Type u_6
f : α → β
x : List α
⊢ List.Vector.traverseAux (pure ∘ f) x = ⟨List.map f x, ⋯⟩

Tactic:
induction x <;> simp! [*, functor_norm] <;> rfl

Result:
no goals

Proof state:
case mk
α β : Type u_6
f : α → β
x : List α
⊢ Vector.traverse (pure ∘ f) ⟨x, ⋯⟩ = pure (map f ⟨x, ⋯⟩)

Tactic:
simp!

Result:
case mk
α β : Type u_6
f : α → β
x : List α
⊢ List.Vector.traverseAux (pure ∘ f) x = ⟨List.map f x, ⋯⟩
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma toUnitHom_eq_char' {a : ZMod n} (ha : IsUnit a) : χ a = χ.toUnitHom ha.unit

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
a : ZMod n
ha : IsUnit a
⊢ χ a = ↑((toUnitHom χ) ha.unit)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Iic
    (hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x)
    (f'int : IntegrableOn f' (Iic a)) (fint : IntegrableOn f (Iic a)) :
    Tendsto f atBot (𝓝 0)

Proof state:
case intro
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (limUnder atBot (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atBot volume
s : Set ℝ
hs : s ∈ atBot
b : ℝ
hb : ∀ b_1 ≤ b, b_1 ∈ s
⊢ ⊤ ≤ volume s

Tactic:
rw [← volume_Iic (a := b)]

Result:
case intro
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (limUnder atBot (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atBot volume
s : Set ℝ
hs : s ∈ atBot
b : ℝ
hb : ∀ b_1 ≤ b, b_1 ∈ s
⊢ volume (Iic b) ≤ volume s

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (limUnder atBot (⇑F ∘ f)))
⊢ Tendsto f atBot (𝓝 0)

Tactic:
have B : limUnder atBot (F ∘ f) = F 0 := by
  have : IntegrableAtFilter (F ∘ f) atBot := by exact ⟨Iic a, Iic_mem_atBot _, Fint⟩
  apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
  intro s hs
  rcases mem_atBot_sets.1 hs with ⟨b, hb⟩
  apply le_antisymm (le_top)
  rw [← volume_Iic (a := b)]
  exact measure_mono hb

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (limUnder atBot (⇑F ∘ f)))
B : limUnder atBot (⇑F ∘ f) = F 0
⊢ Tendsto f atBot (𝓝 0)
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem uniformIntegrable_of [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    (h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0,
      ∀ i, eLpNorm ({ x | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
    UniformIntegrable f p μ

Proof state:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ x ∉ {x | C ≤ ‖g i x‖₊}

Tactic:
rwa [Set.mem_setOf, hx] at hfx

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_irrational : Irrational φ

Proof state:
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ 0.5 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
this : Irrational √↑5
⊢ Irrational φ

Tactic:
have := this.rat_add 1

Result:
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ Irrational φ

Proof state:
⊢ Nat.Prime 5

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ Irrational φ

Tactic:
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)

Result:
this : Irrational √↑5
⊢ Irrational φ

Proof state:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = ↑0.5 * (↑1 + √↑5)

Tactic:
norm_num

Result:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = 1 / 2 * (1 + √5)

Proof state:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = 1 / 2 * (1 + √5)

Tactic:
field_simp

Result:
no goals

Proof state:
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ Irrational φ

Tactic:
convert this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)

Result:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = ↑0.5 * (↑1 + √↑5)
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem isPrimitiveClassified_aux (hc : x.gcd y = 1) (hzpos : 0 < z) {m n : ℤ}
    (hm2n2 : 0 < m ^ 2 + n ^ 2) (hv2 : (x : ℚ) / z = 2 * m * n / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2))
    (hw2 : (y : ℚ) / z = ((m : ℚ) ^ 2 - (n : ℚ) ^ 2) / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2))
    (H : Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1) (co : Int.gcd m n = 1)
    (pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) : h.IsPrimitiveClassified

Proof state:
case h
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2
⊢ x = 2 * m * n

Tactic:
rw [← Rat.coe_int_inj _ _, ← div_left_inj' ((mt (Rat.coe_int_inj z 0).mp) hz), hv2, h2.right]

Result:
case h
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2
⊢ 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2) = ↑(2 * m * n) / ↑(m ^ 2 + n ^ 2)

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
⊢ ↑y / ↑z = ↑(m ^ 2 - n ^ 2) / ↑(m ^ 2 + n ^ 2)

Tactic:
rw [hw2]

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
⊢ (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2) = ↑(m ^ 2 - n ^ 2) / ↑(m ^ 2 + n ^ 2)
-- Mathlib/LinearAlgebra/InvariantBasisNumber.lean
theorem nontrivial_of_invariantBasisNumber : Nontrivial R

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ False

Tactic:
refine zero_ne_one (eq_of_fin_equiv R ?_)

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ ∀ (m : R) (x : Fin 0 → R),
    { toFun := 0, map_add' := ⋯ }.toFun (m • x) = (RingHom.id R) m • { toFun := 0, map_add' := ⋯ }.toFun x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this : Subsingleton R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R

Tactic:
haveI : Subsingleton (Fin 1 → R) :=
  Subsingleton.intro fun a b => funext fun x => Subsingleton.elim _ _

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
⊢ Nontrivial R

Tactic:
by_contra h

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R

Tactic:
exact
  { toFun := 0
    invFun := 0
    map_add' := by simp
    map_smul' := by simp
    left_inv := fun _ => by simp [eq_iff_true_of_subsingleton]
    right_inv := fun _ => by simp [eq_iff_true_of_subsingleton] }

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
x✝ : Fin 1 → R
⊢ { toFun := 0, map_add' := ⋯, map_smul' := ⋯ }.toFun (0 x✝) = x✝

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ ∀ (x y : Fin 0 → R), 0 (x + y) = 0 x + 0 y

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R

Tactic:
haveI := not_nontrivial_iff_subsingleton.1 h

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this : Subsingleton R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
x✝ : Fin 0 → R
⊢ 0 ({ toFun := 0, map_add' := ⋯, map_smul' := ⋯ }.toFun x✝) = x✝

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
theorem compactOpen_eq_iInf_induced :
    (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) =
      ⨅ (K : Set X) (_ : IsCompact K), .induced (.restrict K) ContinuousMap.compactOpen

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ compactOpen = ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen

Tactic:
refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen ≤ compactOpen

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen ≤ compactOpen

Tactic:
refine le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen U}
⊢ IsOpen {f | MapsTo (⇑f) K U}

Proof state:
case h.e'_3
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen U}
⊢ {f | MapsTo (⇑f) K U} = restrict K ⁻¹' {f | MapsTo (⇑f) univ U}

Tactic:
simp [mapsTo_univ_iff, Subtype.forall, MapsTo]

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen U}
⊢ IsOpen {f | MapsTo (⇑f) K U}

Tactic:
convert isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)

Result:
case h.e'_3
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen U}
⊢ {f | MapsTo (⇑f) K U} = restrict K ⁻¹' {f | MapsTo (⇑f) univ U}
-- Mathlib/Data/Int/Init.lean
@[simp] lemma toNat_eq_zero : ∀ {n : ℤ}, n.toNat = 0 ↔ n ≤ 0
  | (n : ℕ) => by simp
  | -[n+1] => by simpa [toNat] using Int.le_of_lt (negSucc_lt_zero n)

Proof state:
n : ℕ
⊢ -[n+1].toNat = 0 ↔ -[n+1] ≤ 0

Tactic:
simpa [toNat] using Int.le_of_lt (negSucc_lt_zero n)

Result:
no goals

Proof state:
n : ℕ
⊢ (↑n).toNat = 0 ↔ ↑n ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
    4 ∣ a + b ∨ 4 ∣ a - b

Proof state:
case intro
b : ℤ
hb : Odd b
m : ℤ
⊢ 4 ∣ 2 * m + 1 + b ∨ 4 ∣ 2 * m + 1 - b

Tactic:
obtain ⟨n, rfl⟩ := hb

Result:
case intro.intro
m n : ℤ
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)

Proof state:
case intro.intro
m n : ℤ
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)

Tactic:
omega

Result:
no goals

Proof state:
a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b

Tactic:
obtain ⟨m, rfl⟩ := ha

Result:
case intro
b : ℤ
hb : Odd b
m : ℤ
⊢ 4 ∣ 2 * m + 1 + b ∨ 4 ∣ 2 * m + 1 - b
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem relIso_enum' {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r]
    [IsWellOrder β s] (f : r ≃r s) (o : Ordinal) :
    ∀ (hr : o < type r) (hs : o < type s), f (enum r ⟨o, hr⟩) = enum s ⟨o, hs⟩

Proof state:
case intro.intro
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f ((enum r) ⟨type t, ⋯⟩) = (enum s) ⟨type t, ⋯⟩

Tactic:
rw [enum_type g, enum_type (g.transRelIso f)]

Result:
case intro.intro
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (g.transRelIso f).top

Proof state:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (hr : o < type r) (hs : o < type s), f ((enum r) ⟨o, hr⟩) = (enum s) ⟨o, hs⟩

Tactic:
refine inductionOn o ?_

Result:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), f ((enum r) ⟨type r_1, hr⟩) = (enum s) ⟨type r_1, hs⟩

Proof state:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), f ((enum r) ⟨type r_1, hr⟩) = (enum s) ⟨type r_1, hs⟩

Tactic:
rintro γ t wo ⟨g⟩ ⟨h⟩

Result:
case intro.intro
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f ((enum r) ⟨type t, ⋯⟩) = (enum s) ⟨type t, ⋯⟩

Proof state:
case intro.intro
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (g.transRelIso f).top

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/Ideal.lean
lemma map_algebraMap_ne_top_iff_disjoint (I : Ideal R) :
    I.map (algebraMap R S) ≠ ⊤ ↔ Disjoint (M : Set R) (I : Set R)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ ¬Disjoint ↑M ↑I ↔ ∃ m ∈ M, m * 1 ∈ I

Tactic:
simp [Set.disjoint_left]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ Ideal.map (algebraMap R S) I ≠ ⊤ ↔ Disjoint ↑M ↑I

Tactic:
simp only [ne_eq, Ideal.eq_top_iff_one, ← map_one (algebraMap R S), not_iff_comm,
  IsLocalization.algebraMap_mem_map_algebraMap_iff M]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ ¬Disjoint ↑M ↑I ↔ ∃ m ∈ M, m * 1 ∈ I
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem mem_ae_map_iff {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) :
    s ∈ ae (μ.map f) ↔ f ⁻¹' s ∈ ae μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ s ∈ ae (map f μ) ↔ f ⁻¹' s ∈ ae μ

Tactic:
simp only [mem_ae_iff, map_apply_of_aemeasurable hf hs.compl, preimage_compl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma binEntropy_nonneg (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : 0 ≤ binEntropy p

Proof state:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ binEntropy p

Tactic:
obtain rfl | hp₀ := hp₀.eq_or_lt

Result:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ binEntropy 0

case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ binEntropy p

Proof state:
case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ binEntropy p

Tactic:
exact (binEntropy_pos hp₀ hp₁).le

Result:
no goals

Proof state:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ binEntropy 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ binEntropy p

Tactic:
obtain rfl | hp₁ := hp₁.eq_or_lt

Result:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ binEntropy 1

case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ binEntropy p

Proof state:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ binEntropy 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_div_flip {α : Type*} [CommGroup α] [LinearOrder α]
    [MulLeftMono α] {a b : α} : a / b ≤ b / a ↔ a ≤ b

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
exact div_le_inv_mul_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ b / a ↔ a ≤ b

Tactic:
rw [div_eq_mul_inv b, mul_comm]

Result:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
lemma id_apply (M : SemiNormedGrp₁) (r : M) :
    (𝟙 M : M ⟶ M) r = r

Proof state:
M : SemiNormedGrp₁
r : M.carrier
⊢ ↑(Hom.hom (𝟙 M)) r = r

Tactic:
simp

Result:
no goals