harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/PGame.lean
/-- A small family of pre-games is bounded above. -/
lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → PGame.{u}) :
    BddAbove (Set.range f)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
⊢ BddAbove (Set.range f)

Tactic:
refine ⟨x, Set.forall_mem_range.2 fun i ↦ ?_⟩

Result:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ f i ≤ x

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
⊢ BddAbove (Set.range f)

Tactic:
let x : PGame.{u} := ⟨Σ i, (f <| (equivShrink.{u} ι).symm i).LeftMoves, PEmpty,
  fun x ↦ moveLeft _ x.2, PEmpty.elim⟩

Result:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
⊢ BddAbove (Set.range f)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ f i ≤ x

Tactic:
rw [← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]

Result:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ (∀ (i_1 : (f ((equivShrink ι).symm ((equivShrink ι) i))).LeftMoves),
      (f ((equivShrink ι).symm ((equivShrink ι) i))).moveLeft i_1 ⧏ x) ∧
    ∀ (j : x.RightMoves), f ((equivShrink ι).symm ((equivShrink ι) i)) ⧏ x.moveRight j

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ (∀ (i_1 : (f ((equivShrink ι).symm ((equivShrink ι) i))).LeftMoves),
      (f ((equivShrink ι).symm ((equivShrink ι) i))).moveLeft i_1 ⧏ x) ∧
    ∀ (j : x.RightMoves), f ((equivShrink ι).symm ((equivShrink ι) i)) ⧏ x.moveRight j

Tactic:
simpa [x] using fun j ↦ @moveLeft_lf x ⟨equivShrink ι i, j⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_add_measure {f : α → G} (hμ : Integrable f μ) (hν : Integrable f ν) :
    ∫ x, f x ∂(μ + ν) = ∫ x, f x ∂μ + ∫ x, f x ∂ν

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν

Tactic:
swap

Result:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν

case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : CompleteSpace G
hfi : Integrable f (μ + ν)
⊢ setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f

Tactic:
have hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ : Set α → G →L[ℝ] G) 1 :=
  DominatedFinMeasAdditive.add_measure_right μ ν (dominatedFinMeasAdditive_weightedSMul μ)
    zero_le_one

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : CompleteSpace G
hfi : Integrable f (μ + ν)
hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ) 1
⊢ setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν

Tactic:
simp [integral, hG]

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem mul_iff : IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)

Tactic:
rwa [mul_comm]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
rw [← mul_and_mul_iff]

Result:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_C {a : R} (a0 : a ≠ 0) : (C a).degree = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a).degree = 0

Tactic:
rw [← mul_one (C a), ← T_zero]

Result:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a * T 0).degree = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a * T 0).degree = 0

Tactic:
exact degree_C_mul_T 0 a a0

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem zero_cpow_eq_iff {x : ℂ} {a : ℂ} : (0 : ℂ) ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case pos
a : ℂ
hyp : (if 0 = 0 then 1 else 0) = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Tactic:
simp only [if_true, eq_self_iff_true] at hyp

Result:
case pos
a : ℂ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Proof state:
case mpr.inr.intro

⊢ 0 ^ 0 = 1

Tactic:
exact cpow_zero _

Result:
no goals

Proof state:
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
simp only [cpow_def, eq_self_iff_true, if_true] at hyp

Result:
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case neg.h
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0

Tactic:
exact ⟨h, hyp.symm⟩

Result:
no goals

Proof state:
case neg
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
left

Result:
case neg.h
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0

Proof state:
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
by_cases h : x = 0

Result:
case pos
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case neg
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case mpr.inl.intro
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

Tactic:
exact zero_cpow h

Result:
no goals

Proof state:
case pos
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
subst h

Result:
case pos
a : ℂ
hyp : (if 0 = 0 then 1 else 0) = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Proof state:
case pos.h
a : ℂ
hyp : 1 = a
⊢ 0 = 0 ∧ a = 1

Tactic:
exact ⟨rfl, hyp.symm⟩

Result:
no goals

Proof state:
case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)

Result:
case mpr.inl.intro
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

case mpr.inr.intro

⊢ 0 ^ 0 = 1

Proof state:
x a : ℂ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor

Result:
case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Proof state:
case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
intro hyp

Result:
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case pos
a : ℂ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Tactic:
right

Result:
case pos.h
a : ℂ
hyp : 1 = a
⊢ 0 = 0 ∧ a = 1

Proof state:
case neg
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [if_neg h] at hyp

Result:
case neg
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equiv_of_X_eq_of_Y_eq {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) : P ≈ Q

Proof state:
case h
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ (fun m => m • Q) (Units.mk0 (P z) hPz / Units.mk0 (Q z) hQz) = P

Tactic:
simp only [Units.smul_def, smul_fin3, Units.val_div_eq_div_val, Units.val_mk0, mul_comm, mul_div,
  ← hx, ← hy, mul_div_cancel_right₀ _ hQz, fin3_def]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ P ≈ Q

Tactic:
use Units.mk0 _ hPz / Units.mk0 _ hQz

Result:
case h
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ (fun m => m • Q) (Units.mk0 (P z) hPz / Units.mk0 (Q z) hQz) = P
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma equivToUnitHom_mul_apply (χ₁ χ₂ : MulChar R R') (a : Rˣ) :
    equivToUnitHom (χ₁ * χ₂) a = equivToUnitHom χ₁ a * equivToUnitHom χ₂ a

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (equivToUnitHom (χ₁ * χ₂)) a = (equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a

Tactic:
apply_fun ((↑) : R'ˣ → R') using Units.ext

Result:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a)

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a) * ↑((equivToUnitHom χ₂) a)

Tactic:
simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a)

Tactic:
push_cast

Result:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a) * ↑((equivToUnitHom χ₂) a)
-- Mathlib/Topology/Homotopy/Product.lean
theorem prod_projLeft_projRight (p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)) :
    prod (projLeft p) (projRight p) = p

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod ⟦a✝.map ⋯⟧ ⟦a✝.map ⋯⟧ = ⟦a✝⟧

Tactic:
congr

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft ⟦a✝⟧) (projRight ⟦a✝⟧) = ⟦a✝⟧

Tactic:
simp only [projLeft, projRight, ← Path.Homotopic.map_lift, prod_lift]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod ⟦a✝.map ⋯⟧ ⟦a✝.map ⋯⟧ = ⟦a✝⟧

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p

Tactic:
induction p using Quotient.inductionOn

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft ⟦a✝⟧) (projRight ⟦a✝⟧) = ⟦a✝⟧
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_eq_zero_iff {u : V} {p : G.Walk u u} : p.length = 0 ↔ p = nil

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.length = 0 ↔ p = nil

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunction_le (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ n, f n → g n) :
    cantorFunction c f ≤ cantorFunction c g

Proof state:
case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
replace h3 : g n = true := h3 n h

Result:
case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Proof state:
case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
simp [h, h3]

Result:
no goals

Proof state:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
cases h : f n

Result:
case false
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Proof state:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i

Tactic:
intro n

Result:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Proof state:
case false
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
simp [h, cantorFunctionAux_nonneg h1]

Result:
no goals

Proof state:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ cantorFunction c f ≤ cantorFunction c g

Tactic:
apply tsum_le_tsum _ (summable_cantor_function f h1 h2) (summable_cantor_function g h1 h2)

Result:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Set.Countable.isLindelof_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Countable)
    (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)

Proof state:
case h.right.h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i_2 ∈ ⋃ i_3 ∈ s, r i_3, U i_2

Tactic:
intro i is

Result:
case h.right.h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i✝ : Type u
U : i✝ → Set X
hU : ∀ (i : i✝), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i
r : ι → Set i✝
hr : ∀ i ∈ s, (r i).Countable ∧ f i ⊆ ⋃ i_1 ∈ r i, U i_1
i : ι
is : i ∈ s
⊢ f i ⊆ ⋃ i ∈ ⋃ i ∈ s, r i, U i

Proof state:
case h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ (⋃ i_1 ∈ s, r i_1).Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ ⋃ i_2 ∈ s, r i_2, U i_1

Tactic:
constructor

Result:
case h.left
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ (⋃ i_1 ∈ s, r i_1).Countable

case h.right
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ ⋃ i_2 ∈ s, r i_2, U i_1

Proof state:
case h.right
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ ⋃ i_2 ∈ s, r i_2, U i_1

Tactic:
refine iUnion₂_subset ?h.right.h

Result:
case h.right.h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i_2 ∈ ⋃ i_3 ∈ s, r i_3, U i_2
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem comp_P_eq_self {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) :
    φ ≫ (P q).f (n + 1) = φ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a, ⋯⟩.succ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

Tactic:
simp only [Fin.succ_mk] at eq

Result:
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a + 1, ⋯⟩ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem cancel_left {f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : Injective f) :
    f.comp g₁ = f.comp g₂ ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_le_one : √x ≤ 1 ↔ x ≤ 1

Proof state:
x : ℝ
⊢ √x ≤ 1 ↔ x ≤ 1

Tactic:
rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem if_true_right [h : Decidable p] :
    ite p q True ↔ p → q

Proof state:
p q : Prop
h : Decidable p
⊢ (if p then q else True) ↔ p → q

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals

Proof state:
case isTrue
p q : Prop
h✝ : p
⊢ (if p then q else True) ↔ p → q

Tactic:
rename_i g

Result:
case isTrue
p q : Prop
g : p
⊢ (if p then q else True) ↔ p → q

Proof state:
case isTrue
p q : Prop
g : p
⊢ (if p then q else True) ↔ p → q

Tactic:
simp [g]

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem Topology.IsOpenEmbedding.compatiblePreserving (hf : IsOpenEmbedding f) :
    CompatiblePreserving (Opens.grothendieckTopology Y) hf.isOpenMap.functor

Proof state:
case hF
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ {c : Opens ↑X} → {d : Opens ↑Y} → (d ⟶ ⋯.functor.obj c) → (c' : Opens ↑X) × (⋯.functor.obj c' ≅ d)

Tactic:
intro U V i

Result:
case hF
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ ⋯.functor.obj U
⊢ (c' : Opens ↑X) × (⋯.functor.obj c' ≅ V)

Proof state:
case hF.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ ⋯.functor.obj U
w✝ : ↑X
left✝ : w✝ ∈ ↑U
h : (ConcreteCategory.hom f) w✝ ∈ V.1
⊢ (ConcreteCategory.hom f) w✝ ∈ Set.range ⇑(ConcreteCategory.hom f)

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor

Tactic:
haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.injective

Result:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor

Tactic:
apply compatiblePreservingOfDownwardsClosed

Result:
case hF
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ {c : Opens ↑X} → {d : Opens ↑Y} → (d ⟶ ⋯.functor.obj c) → (c' : Opens ↑X) × (⋯.functor.obj c' ≅ d)

Proof state:
case hF
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ ⋯.functor.obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f)

Tactic:
obtain ⟨_, _, rfl⟩ := i.le h

Result:
case hF.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ ⋯.functor.obj U
w✝ : ↑X
left✝ : w✝ ∈ ↑U
h : (ConcreteCategory.hom f) w✝ ∈ V.1
⊢ (ConcreteCategory.hom f) w✝ ∈ Set.range ⇑(ConcreteCategory.hom f)

Proof state:
case hF
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ ⋯.functor.obj U
⊢ (c' : Opens ↑X) × (⋯.functor.obj c' ≅ V)

Tactic:
refine ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ ?_⟩

Result:
case hF
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ ⋯.functor.obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f)