harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/UpperLower/Basic.lean
theorem IsUpperSet.total (hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ t ∨ t ⊆ s

Proof state:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
a : α
has : a ∈ s
hat : a ∉ t
b : α
hbt : b ∈ t
hbs : b ∉ s
hab : a ≤ b
⊢ False

Tactic:
exact hbs (hs hab has)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
h : (∃ a ∈ s, a ∉ t) ∧ ∃ a ∈ t, a ∉ s
⊢ False

Tactic:
obtain ⟨⟨a, has, hat⟩, b, hbt, hbs⟩ := h

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
a : α
has : a ∈ s
hat : a ∉ t
b : α
hbt : b ∈ t
hbs : b ∉ s
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
h : ¬s ⊆ t ∧ ¬t ⊆ s
⊢ False

Tactic:
simp_rw [Set.not_subset] at h

Result:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
h : (∃ a ∈ s, a ∉ t) ∧ ∃ a ∈ t, a ∉ s
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
⊢ s ⊆ t ∨ t ⊆ s

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
h : ¬s ⊆ t ∧ ¬t ⊆ s
⊢ False

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
a : α
has : a ∈ s
hat : a ∉ t
b : α
hbt : b ∈ t
hbs : b ∉ s
⊢ False

Tactic:
obtain hab | hba := le_total a b

Result:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
a : α
has : a ∈ s
hat : a ∉ t
b : α
hbt : b ∈ t
hbs : b ∉ s
hab : a ≤ b
⊢ False

case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
a : α
has : a ∈ s
hat : a ∉ t
b : α
hbt : b ∈ t
hbs : b ∉ s
hba : b ≤ a
⊢ False

Proof state:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
a : α
has : a ∈ s
hat : a ∉ t
b : α
hbt : b ∈ t
hbs : b ∉ s
hba : b ≤ a
⊢ False

Tactic:
exact hat (ht hba hbt)

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem exists_rat_eq_nth_conv : ∃ q : ℚ, (of v).convs n = (q : K)

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
Bₙ : ℚ
nth_den_eq : (of v).dens n = ↑Bₙ
⊢ ∃ q, (of v).convs n = ↑q

Tactic:
use Aₙ / Bₙ

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
Bₙ : ℚ
nth_den_eq : (of v).dens n = ↑Bₙ
⊢ (of v).convs n = ↑(Aₙ / Bₙ)

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
Bₙ : ℚ
nth_den_eq : (of v).dens n = ↑Bₙ
⊢ (of v).convs n = ↑(Aₙ / Bₙ)

Tactic:
simp [nth_num_eq, nth_den_eq, conv_eq_num_div_den]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, (of v).convs n = ↑q

Tactic:
rcases exists_rat_eq_nth_num v n with ⟨Aₙ, nth_num_eq⟩

Result:
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
⊢ ∃ q, (of v).convs n = ↑q

Proof state:
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
⊢ ∃ q, (of v).convs n = ↑q

Tactic:
rcases exists_rat_eq_nth_den v n with ⟨Bₙ, nth_den_eq⟩

Result:
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
Bₙ : ℚ
nth_den_eq : (of v).dens n = ↑Bₙ
⊢ ∃ q, (of v).convs n = ↑q
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem tendsto_log_comp_add_sub_log (y : ℝ) :
    Tendsto (fun x : ℝ => log (x + y) - log x) atTop (𝓝 0)

Proof state:
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)

Tactic:
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]

Result:
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (rexp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))

Proof state:
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (rexp ∘ fun x => log (x + y) - log x) x

Tactic:
rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div] <;> linarith

Result:
no goals

Proof state:
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x => 1 + y / x) =ᶠ[atTop] rexp ∘ fun x => log (x + y) - log x

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy

Result:
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (rexp ∘ fun x => log (x + y) - log x) x

Proof state:
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (rexp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))

Tactic:
refine this.congr' ?_

Result:
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x => 1 + y / x) =ᶠ[atTop] rexp ∘ fun x => log (x + y) - log x

Proof state:
y : ℝ
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)

Tactic:
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0)) :=
  tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)

Result:
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
-- Mathlib/Probability/Independence/Basic.lean
theorem indepFun_iff_measure_inter_preimage_eq_mul {mβ : MeasurableSpace β}
    {mβ' : MeasurableSpace β'} :
    IndepFun f g μ ↔
      ∀ s t, MeasurableSet s → MeasurableSet t
        → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)

Proof state:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
⊢ IndepFun f g μ ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)

Tactic:
simp only [IndepFun, Kernel.indepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq,
  Filter.eventually_pure, Kernel.const_apply]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem p_nonnunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ nonunits ℤ_[p]

Tactic:
have : (p : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp.out.one_lt

Result:
p : ℕ
hp : Fact (Nat.Prime p)
this : (↑p)⁻¹ < 1
⊢ ↑p ∈ nonunits ℤ_[p]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
this : (↑p)⁻¹ < 1
⊢ ↑p ∈ nonunits ℤ_[p]

Tactic:
rwa [← norm_p, ← mem_nonunits] at this

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean
theorem ZMod.charpoly_pow_card {p : ℕ} [Fact p.Prime] (M : Matrix n n (ZMod p)) :
    (M ^ p).charpoly = M.charpoly

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).charpoly = M.charpoly
⊢ (M ^ p).charpoly = M.charpoly

Tactic:
rwa [ZMod.card] at h

Result:
no goals

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ (M ^ p).charpoly = M.charpoly

Tactic:
have h := FiniteField.Matrix.charpoly_pow_card M

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).charpoly = M.charpoly
⊢ (M ^ p).charpoly = M.charpoly
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem LindelofSpace.elim_nhds_subcover [LindelofSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ

Proof state:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ

Tactic:
use t, tc

Result:
case right
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ⋃ x ∈ t, U x = univ

Proof state:
case right
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ⋃ x ∈ t, U x = univ

Tactic:
apply top_unique s

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ

Tactic:
obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x

Result:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_of_Z_eq_zero {P : Fin 3 → F} (hPz : P z = 0) : toAffine W P = 0

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z = 0
⊢ toAffine W P = 0

Tactic:
rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem exists_succ_nth_stream_of_fr_zero {ifp_succ_n : IntFractPair K}
    (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n)
    (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) :
    ∃ ifp_n : IntFractPair K, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Tactic:
simpa only [IntFractPair.of, Int.fract, sub_eq_zero] using succ_nth_fr_eq_zero

Result:
no goals

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Tactic:
refine ⟨ifp_n, seq_nth_eq, ?_⟩

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Tactic:
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with
  ⟨ifp_n, seq_nth_eq, _, rfl⟩

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
-- Mathlib/CategoryTheory/Action/Monoidal.lean
theorem tensorUnit_ρ {g : G} :
    @DFunLike.coe (G →* End (𝟙_ V)) _ _ _ (𝟙_ (Action V G)).ρ g = 𝟙 (𝟙_ V)

Proof state:
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
inst✝ : MonoidalCategory V
g : G
⊢ (𝟙_ (Action V G)).ρ g = 𝟙 (𝟙_ V)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem mem_support_iff {u v w : V} (p : G.Walk u v) :
    w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem range_add_eq_union : range (a + b) = range a ∪ (range b).map (addLeftEmbedding a)

Proof state:
a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
rw [Finset.range_eq_Ico, map_eq_image]

Result:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a)) (Ico 0 b)

Proof state:
case h.e'_3.h.e'_4
a b : ℕ
⊢ image (⇑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)

Tactic:
ext x

Result:
case h.e'_3.h.e'_4.h
a b x : ℕ
⊢ x ∈ image (⇑(addLeftEmbedding a)) (Ico 0 b) ↔ x ∈ Ico a (a + b)

Proof state:
a b x : ℕ
h : a ≤ x ∧ x < a + b
⊢ x - a < b ∧ a + (x - a) = x

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_3.h.e'_4.h
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b

Tactic:
constructor

Result:
case h.e'_3.h.e'_4.h.mp
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b

case h.e'_3.h.e'_4.h.mpr
a b x : ℕ
⊢ a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x

Proof state:
case h.e'_3.h.e'_4.h
a b x : ℕ
⊢ x ∈ image (⇑(addLeftEmbedding a)) (Ico 0 b) ↔ x ∈ Ico a (a + b)

Tactic:
simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]

Result:
case h.e'_3.h.e'_4.h
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b

Proof state:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a)) (Ico 0 b)

Tactic:
convert (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm

Result:
case h.e'_3.h.e'_4
a b : ℕ
⊢ image (⇑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)

Proof state:
case h.e'_3.h.e'_4.h.mpr
a b x : ℕ
⊢ a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x

Tactic:
rintro h

Result:
case h.e'_3.h.e'_4.h.mpr
a b x : ℕ
h : a ≤ x ∧ x < a + b
⊢ ∃ a_1 < b, a + a_1 = x

Proof state:
case h.e'_3.h.e'_4.h.mpr
a b x : ℕ
h : a ≤ x ∧ x < a + b
⊢ ∃ a_1 < b, a + a_1 = x

Tactic:
exact ⟨x - a, by omega⟩

Result:
no goals

Proof state:
case h.e'_3.h.e'_4.h.mp
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem monotone_iff_map_nonneg [iamhc : AddMonoidHomClass F α β] :
    Monotone (f : α → β) ↔ ∀ a, 0 ≤ a → 0 ≤ f a :=
  ⟨fun h a => by
    rw [← map_zero f]
    apply h, fun h a b hl => by
    rw [← sub_add_cancel b a, map_add f]
    exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)⟩

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedAddCommGroup α
inst✝ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 ≤ a → 0 ≤ f a
a b : α
hl : a ≤ b
⊢ f a ≤ f (b - a) + f a

Tactic:
exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedAddCommGroup α
inst✝ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 ≤ a → 0 ≤ f a
a b : α
hl : a ≤ b
⊢ f a ≤ f b

Tactic:
rw [← sub_add_cancel b a, map_add f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedAddCommGroup α
inst✝ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 ≤ a → 0 ≤ f a
a b : α
hl : a ≤ b
⊢ f a ≤ f (b - a) + f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedAddCommGroup α
inst✝ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → 0 ≤ f a

Tactic:
rw [← map_zero f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedAddCommGroup α
inst✝ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → f 0 ≤ f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedAddCommGroup α
inst✝ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → f 0 ≤ f a

Tactic:
apply h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : Array α) :
    countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l

Proof state:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
toList✝ : List α
⊢ countP p (filterMap f { toList := toList✝ }) = countP (fun a => (Option.map p (f a)).getD false) { toList := toList✝ }

Tactic:
simp [List.countP_filterMap]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : Array α
⊢ countP p (filterMap f l) = countP (fun a => (Option.map p (f a)).getD false) l

Tactic:
cases l

Result:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
toList✝ : List α
⊢ countP p (filterMap f { toList := toList✝ }) = countP (fun a => (Option.map p (f a)).getD false) { toList := toList✝ }
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem image_symm_eq_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) :
    e.symm '' s = e ⁻¹' s

Proof state:
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
rw [e.symm.image_eq_preimage, e.symm_symm]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_zero_left (a) : nfp 0 a = a

Proof state:
case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ (0 ∘ 0^[n✝]) a ≤ 0^[0] a

Tactic:
simp

Result:
no goals

Proof state:
case zero
a : Ordinal.{u_1}
⊢ 0^[0] a ≤ 0^[0] a

Tactic:
rfl

Result:
no goals

Proof state:
case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ 0^[n✝ + 1] a ≤ 0^[0] a

Tactic:
rw [Function.iterate_succ']

Result:
case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ (0 ∘ 0^[n✝]) a ≤ 0^[0] a

Proof state:
a : Ordinal.{u_1}
n : ℕ
⊢ 0^[n] a ≤ 0^[0] a

Tactic:
cases n

Result:
case zero
a : Ordinal.{u_1}
⊢ 0^[0] a ≤ 0^[0] a

case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ 0^[n✝ + 1] a ≤ 0^[0] a

Proof state:
a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a

Tactic:
apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)

Result:
a : Ordinal.{u_1}
⊢ ∀ (i : ℕ), 0^[i] a ≤ 0^[0] a

Proof state:
a : Ordinal.{u_1}
⊢ ∀ (i : ℕ), 0^[i] a ≤ 0^[0] a

Tactic:
intro n

Result:
a : Ordinal.{u_1}
n : ℕ
⊢ 0^[n] a ≤ 0^[0] a

Proof state:
a : Ordinal.{u_1}
⊢ nfp 0 a = a

Tactic:
rw [← iSup_iterate_eq_nfp]

Result:
a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a
-- Mathlib/Topology/Constructions.lean
theorem nhds_eq (x : CofiniteTopology X) : 𝓝 x = pure x ⊔ cofinite

Proof state:
case h
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite

Tactic:
rw [mem_nhds_iff]

Result:
case h
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, IsOpen t ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite

Proof state:
case h.mpr.intro
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
hU : x ∈ U
hU' : Uᶜ.Finite
⊢ ∃ t ⊆ U, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨U, Subset.rfl, fun _ => hU', hU⟩

Result:
no goals

Proof state:
X : Type u
x : CofiniteTopology X
⊢ 𝓝 x = pure x ⊔ cofinite

Tactic:
ext U

Result:
case h
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite

Proof state:
case h.mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, IsOpen t ∧ x ∈ t

Tactic:
rintro ⟨hU : x ∈ U, hU' : Uᶜ.Finite⟩

Result:
case h.mpr.intro
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
hU : x ∈ U
hU' : Uᶜ.Finite
⊢ ∃ t ⊆ U, IsOpen t ∧ x ∈ t

Proof state:
case h
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, IsOpen t ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite

Tactic:
constructor

Result:
case h.mp
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, IsOpen t ∧ x ∈ t) → U ∈ pure x ⊔ cofinite

case h.mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, IsOpen t ∧ x ∈ t

Proof state:
case h.mp.intro.intro.intro
X : Type u
x : CofiniteTopology X
U V : Set (CofiniteTopology X)
hVU : V ⊆ U
V_op : IsOpen V
haV : x ∈ V
⊢ U ∈ pure x ⊔ cofinite

Tactic:
exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩

Result:
no goals

Proof state:
case h.mp
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, IsOpen t ∧ x ∈ t) → U ∈ pure x ⊔ cofinite

Tactic:
rintro ⟨V, hVU, V_op, haV⟩

Result:
case h.mp.intro.intro.intro
X : Type u
x : CofiniteTopology X
U V : Set (CofiniteTopology X)
hVU : V ⊆ U
V_op : IsOpen V
haV : x ∈ V
⊢ U ∈ pure x ⊔ cofinite
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem apply_one_path : (πₘ (TopCat.ofHom g)).map p = hcast (H.apply_one x₀).symm ≫
    (πₘ (TopCat.ofHom H.uliftMap)).map
      (prodToProdTopI (𝟙 (@fromTop (TopCat.of _) (ULift.up 1))) p) ≫
    hcast (H.apply_one x₁) :=
  Quotient.inductionOn p fun p' => by
    apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H.uliftMap (((Path.refl { down := 1 }).prod p') t✝)

Tactic:
rw [Path.prod_coe, ulift_apply H]

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H (((Path.refl { down := 1 }) t✝).down, p' t✝)

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H (((Path.refl { down := 1 }) t✝).down, p' t✝)

Tactic:
simp

Result:
no goals

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ ∀ (t : ↑I), g (p' t) = H.uliftMap (((Path.refl { down := 1 }).prod p') t)

Tactic:
intros

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H.uliftMap (((Path.refl { down := 1 }).prod p') t✝)

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom g)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ ∀ (t : ↑I), g (p' t) = H.uliftMap (((Path.refl { down := 1 }).prod p') t)