harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.openCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) :
    openCell n j ⊆ C

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ openCell n j ⊆ C

Tactic:
apply subset_trans (openCell_subset_skeleton _ _)
  (by simp_rw [← skeleton_top (C := C) (D := D)]; exact skeleton_mono le_top)

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ skeleton C ↑n ⊆ C

Tactic:
simp_rw [← skeleton_top (C := C) (D := D)]

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ skeleton C ↑n ⊆ skeleton C ⊤

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ skeleton C ↑n ⊆ skeleton C ⊤

Tactic:
exact skeleton_mono le_top

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem insert_union (a : α) (s t : Finset α) : insert a s ∪ t = insert a (s ∪ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ insert a s ∪ t = insert a (s ∪ t)

Tactic:
simp only [insert_eq, union_assoc]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem leftLim_eq_of_tendsto [hα : TopologicalSpace α] [h'α : OrderTopology α] [T2Space β]
    {f : α → β} {a : α} {y : β} (h : 𝓝[<] a ≠ ⊥) (h' : Tendsto f (𝓝[<] a) (𝓝 y)) :
    leftLim f a = y

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ limUnder (𝓝[<] a) f = y

Tactic:
haveI := neBot_iff.2 h

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
this : (𝓝[<] a).NeBot
⊢ limUnder (𝓝[<] a) f = y

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y

Tactic:
have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = y

Tactic:
simp only [leftLim, h, h'', not_true, or_self_iff, if_false]

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ limUnder (𝓝[<] a) f = y

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
this : (𝓝[<] a).NeBot
⊢ limUnder (𝓝[<] a) f = y

Tactic:
exact lim_eq h'

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem not_differentiableAt_abs_zero : ¬ DifferentiableAt ℝ (abs : ℝ → ℝ) 0

Proof state:
h : DifferentiableAt ℝ abs 0
⊢ False

Tactic:
have h₁ : deriv abs (0 : ℝ) = 1 :=
  (uniqueDiffOn_Ici _ _ Set.left_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
    (hasDerivWithinAt_id _ _).congr_of_mem (fun _ h ↦ abs_of_nonneg h) Set.left_mem_Ici

Result:
h : DifferentiableAt ℝ abs 0
h₁ : deriv abs 0 = 1
⊢ False

Proof state:
h : DifferentiableAt ℝ abs 0
h₁ : deriv abs 0 = 1
⊢ False

Tactic:
have h₂ : deriv abs (0 : ℝ) = -1 :=
  (uniqueDiffOn_Iic _ _ Set.right_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
    (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.right_mem_Iic

Result:
h : DifferentiableAt ℝ abs 0
h₁ : deriv abs 0 = 1
h₂ : deriv abs 0 = -1
⊢ False

Proof state:
h : DifferentiableAt ℝ abs 0
h₁ : deriv abs 0 = 1
h₂ : deriv abs 0 = -1
⊢ False

Tactic:
linarith

Result:
no goals

Proof state:
⊢ ¬DifferentiableAt ℝ abs 0

Tactic:
intro h

Result:
h : DifferentiableAt ℝ abs 0
⊢ False
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem isPiSystem_Ici_rat : IsPiSystem (⋃ a : ℚ, {Ici (a : ℝ)})

Proof state:
⊢ IsPiSystem (⋃ a, {Ici ↑a})

Tactic:
convert isPiSystem_image_Ici (((↑) : ℚ → ℝ) '' univ)

Result:
case h.e'_2

⊢ ⋃ a, {Ici ↑a} = Ici '' (Rat.cast '' univ)

Proof state:
case h.e'_2

⊢ ⋃ a, {Ici ↑a} = Ici '' (Rat.cast '' univ)

Tactic:
ext x

Result:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Ici ↑a} ↔ x ∈ Ici '' (Rat.cast '' univ)

Proof state:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Ici ↑a} ↔ x ∈ Ici '' (Rat.cast '' univ)

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasFDerivAt.abs (hf : HasFDerivAt f f' x)
    (h₀ : f x ≠ 0) : HasFDerivAt (fun x ↦ |f x|) ((SignType.sign (f x) : ℝ) • f') x

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
y : E
⊢ (↑(SignType.sign (f x)) • f') y = ((ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f') y

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasFDerivAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') x

Tactic:
convert (hasDerivAt_abs h₀).hasFDerivAt.comp x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
⊢ ↑(SignType.sign (f x)) • f' = (ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f'

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
⊢ ↑(SignType.sign (f x)) • f' = (ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f'

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
y : E
⊢ (↑(SignType.sign (f x)) • f') y = ((ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f') y
-- Mathlib/SetTheory/Game/Basic.lean
theorem not_lf : ∀ {x y : Game}, ¬Game.LF x y ↔ y ≤ x

Proof state:
case mk.mk
x✝ : Game
x : PGame
y✝ : Game
y : PGame
⊢ ¬LF (Quot.mk (⇑setoid) x) (Quot.mk (⇑setoid) y) ↔ Quot.mk (⇑setoid) y ≤ Quot.mk (⇑setoid) x

Tactic:
exact PGame.not_lf

Result:
no goals

Proof state:
⊢ ∀ {x y : Game}, ¬x.LF y ↔ y ≤ x

Tactic:
rintro ⟨x⟩ ⟨y⟩

Result:
case mk.mk
x✝ : Game
x : PGame
y✝ : Game
y : PGame
⊢ ¬LF (Quot.mk (⇑setoid) x) (Quot.mk (⇑setoid) y) ↔ Quot.mk (⇑setoid) y ≤ Quot.mk (⇑setoid) x
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem card_Ioo_eq_card_Icc_sub_two (a b : α) : #(Ioo a b) = #(Icc a b) - 2

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Icc a b) - 1 - 1 = #(Icc a b) - 2

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Icc a b) - 2

Tactic:
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]

Result:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Icc a b) - 1 - 1 = #(Icc a b) - 2
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem diam_Ioc {a b : ℝ} (h : a ≤ b) : Metric.diam (Ioc a b) = b - a

Proof state:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioc a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem coeff_divX : (divX p).coeff n = p.coeff (n + 1)

Proof state:
case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ }.divX.coeff n = { toFinsupp := toFinsupp✝ }.coeff (1 + n)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (n + 1)

Tactic:
rw [add_comm]

Result:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (1 + n)

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (1 + n)

Tactic:
cases p

Result:
case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ }.divX.coeff n = { toFinsupp := toFinsupp✝ }.coeff (1 + n)
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNorm'_add_le (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (hq1 : 1 ≤ q) : eLpNorm' (f + g) q μ ≤ eLpNorm' f q μ + eLpNorm' g q μ :=
  calc
    (∫⁻ a, (‖(f + g) a‖₊ : ℝ≥0∞) ^ q ∂μ) ^ (1 / q) ≤
        (∫⁻ a, ((fun a => (‖f a‖₊ : ℝ≥0∞)) + fun a => (‖g a‖₊ : ℝ≥0∞)) a ^ q ∂μ) ^ (1 / q)

Proof state:
case h₁.hfg.h₁
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
q : ℝ
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
a : α
⊢ ↑‖(f + g) a‖₊ ≤ ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a

Tactic:
simp only [Pi.add_apply, ← ENNReal.coe_add, ENNReal.coe_le_coe, nnnorm_add_le]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
q : ℝ
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
⊢ (∫⁻ (a : α), ↑‖(f + g) a‖₊ ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr with a

Result:
case h₁.hfg.h₁
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
q : ℝ
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
a : α
⊢ ↑‖(f + g) a‖₊ ≤ ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_relrank_comap_comap_eq_lift_relrank_inf (f : L →+* E) :
    lift.{v} (relrank (A.comap f) (B.comap f)) =
    lift.{w} (relrank A (B ⊓ f.fieldRange))

Proof state:
case e_c.h
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ A ⊓ f.fieldRange ⊓ (B ⊓ f.fieldRange) = A ⊓ (B ⊓ f.fieldRange)

Tactic:
rw [inf_assoc, inf_left_comm _ B, inf_of_le_left (le_refl _)]

Result:
no goals

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ lift.{v, w} ((comap f A).relrank (comap f B)) = lift.{w, v} (A.relrank (B ⊓ f.fieldRange))

Tactic:
conv_lhs => rw [← lift_relrank_map_map _ _ f, map_comap_eq, map_comap_eq]

Result:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ lift.{w, v} ((A ⊓ f.fieldRange).relrank (B ⊓ f.fieldRange)) = lift.{w, v} (A.relrank (B ⊓ f.fieldRange))

Proof state:
case e_c
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ (A ⊓ f.fieldRange).relrank (B ⊓ f.fieldRange) = A.relrank (B ⊓ f.fieldRange)

Tactic:
apply relrank_eq_of_inf_eq

Result:
case e_c.h
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ A ⊓ f.fieldRange ⊓ (B ⊓ f.fieldRange) = A ⊓ (B ⊓ f.fieldRange)

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ lift.{w, v} ((A ⊓ f.fieldRange).relrank (B ⊓ f.fieldRange)) = lift.{w, v} (A.relrank (B ⊓ f.fieldRange))

Tactic:
congr 1

Result:
case e_c
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ (A ⊓ f.fieldRange).relrank (B ⊓ f.fieldRange) = A.relrank (B ⊓ f.fieldRange)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
lemma ContDiffWithinAt.analyticOn (h : ContDiffWithinAt 𝕜 ω f s x) :
    ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Proof state:
case intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
exact ⟨u, hu, hp.analyticOn (h'p 0)⟩

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := h

Result:
case intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.iff_to_or (a b : Bool)
    : ((a = true) ↔ (b = true)) = (((!a || b) && (!b || a)) = true)

Proof state:
a b : Bool
⊢ (a = true ↔ b = true) = (((!a || b) && (!b || a)) = true)

Tactic:
revert a b

Result:
⊢ ∀ (a b : Bool), (a = true ↔ b = true) = (((!a || b) && (!b || a)) = true)

Proof state:
⊢ ∀ (a b : Bool), (a = true ↔ b = true) = (((!a || b) && (!b || a)) = true)

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _

Proof state:
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : C
⊢ (whiskerRight adj.unit F ≫ whiskerLeft F adj.counit).app x✝ = (𝟙 (𝟭 C ⋙ F)).app x✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
⊢ whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 (𝟭 C ⋙ F)

Tactic:
ext

Result:
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : C
⊢ (whiskerRight adj.unit F ≫ whiskerLeft F adj.counit).app x✝ = (𝟙 (𝟭 C ⋙ F)).app x✝
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_zero' (hq0_ne : q ≠ 0) (hμ : μ ≠ 0) : eLpNorm' (0 : α → F) q μ = 0

Proof state:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq0 : 0 ≤ q
⊢ eLpNorm' 0 q μ = 0

Tactic:
exact eLpNorm'_zero (lt_of_le_of_ne hq0 hq0_ne.symm)

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hq0_ne : q ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm' 0 q μ = 0

Tactic:
rcases le_or_lt 0 q with hq0 | hq_neg

Result:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq0 : 0 ≤ q
⊢ eLpNorm' 0 q μ = 0

case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq_neg : q < 0
⊢ eLpNorm' 0 q μ = 0

Proof state:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq_neg : q < 0
⊢ eLpNorm' 0 q μ = 0

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, ENNReal.rpow_eq_zero_iff, hμ, hq_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem measurable_measure_prod_mk_left [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
    Measurable fun x => ν (Prod.mk x ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ∑' (i : ℕ), (sfiniteSeq ν i) (Prod.mk x ⁻¹' s)

Tactic:
exact Measurable.ennreal_tsum (fun i ↦ measurable_measure_prod_mk_left_finite hs)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' s)

Tactic:
rw [← sum_sfiniteSeq ν]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => (sum (sfiniteSeq ν)) (Prod.mk x ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => (sum (sfiniteSeq ν)) (Prod.mk x ⁻¹' s)

Tactic:
simp_rw [Measure.sum_apply_of_countable]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ∑' (i : ℕ), (sfiniteSeq ν i) (Prod.mk x ⁻¹' s)
-- Mathlib/Data/Seq/Seq.lean
theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
  ⟨eq_or_mem_of_mem_cons, by rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]⟩

Proof state:
α : Type u
a b : α
s : Seq α
⊢ a = b ∨ a ∈ s → a ∈ cons b s

Tactic:
rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem comp_nullHomotopicMap (f : C ⟶ D) (hom : ∀ i j, D.X i ⟶ E.X j) :
    f ≫ nullHomotopicMap hom = nullHomotopicMap fun i j => f.f i ≫ hom i j

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
⊢ f.f n ≫ (D.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ E.dTo n) =
    C.dFrom n ≫ f.f (c.next n) ≫ hom (c.next n) n + (f.f n ≫ hom n (c.prev n)) ≫ E.dTo n

Tactic:
simp only [Preadditive.comp_add, assoc, f.comm_assoc]

Result:
no goals

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
⊢ (f ≫ nullHomotopicMap hom).f n = (nullHomotopicMap fun i j => f.f i ≫ hom i j).f n

Tactic:
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
⊢ f.f n ≫ (D.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ E.dTo n) =
    C.dFrom n ≫ f.f (c.next n) ≫ hom (c.next n) n + (f.f n ≫ hom n (c.prev n)) ≫ E.dTo n

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
⊢ f ≫ nullHomotopicMap hom = nullHomotopicMap fun i j => f.f i ≫ hom i j

Tactic:
ext n

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
⊢ (f ≫ nullHomotopicMap hom).f n = (nullHomotopicMap fun i j => f.f i ≫ hom i j).f n
-- Mathlib/Analysis/Convex/Topology.lean
theorem Set.Finite.isCompact_convexHull {s : Set E} (hs : s.Finite) :
    IsCompact (convexHull ℝ s)

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
⊢ IsCompact (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex ℝ ↑s)

Tactic:
apply (@isCompact_stdSimplex _ hs.fintype).image

Result:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
⊢ Continuous ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x)

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
⊢ Continuous ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x)

Tactic:
haveI := hs.fintype

Result:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
this : Fintype ↑s
⊢ Continuous ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x)

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
⊢ IsCompact ((convexHull ℝ) s)

Tactic:
rw [hs.convexHull_eq_image]

Result:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
⊢ IsCompact (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex ℝ ↑s)

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : s.Finite
this : Fintype ↑s
⊢ Continuous ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x)

Tactic:
apply LinearMap.continuous_on_pi

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosedMap_sumElim {f : X → Z} {g : Y → Z} :
    IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

Tactic:
simp only [isClosedMap_sum, Sum.elim_inl, Sum.elim_inr]

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_sublist_right {n k : ℕ} (h : k ≠ 0) :
    n.primeFactorsList <+ (n * k).primeFactorsList

Proof state:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList

Tactic:
exact (sublist_append_left _ _).subperm

Result:
no goals

Proof state:
case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList

Tactic:
apply sublist_of_subperm_of_sorted _ (primeFactorsList_sorted _) (primeFactorsList_sorted _)

Result:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList

Proof state:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList

Tactic:
simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]

Result:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList

Proof state:
case zero
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList

Tactic:
simp [zero_mul]

Result:
no goals

Proof state:
n k : ℕ
h : k ≠ 0
⊢ n.primeFactorsList <+ (n * k).primeFactorsList

Tactic:
rcases n with - | hn

Result:
case zero
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList

case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList