harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem compl_neighborFinset_sdiff_inter_eq {v w : V} :
    (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) =
      ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Proof state:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w a✝ : V
⊢ a✝ ∉ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) ↔
    a✝ ∉ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Tactic:
simp [imp_iff_not_or, or_assoc, or_comm, or_left_comm]

Result:
no goals

Proof state:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w a✝ : V
⊢ a✝ ∈ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) ↔
    a✝ ∈ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Tactic:
rw [← not_iff_not]

Result:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w a✝ : V
⊢ a✝ ∉ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) ↔
    a✝ ∉ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) =
    ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Tactic:
ext

Result:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w a✝ : V
⊢ a✝ ∈ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) ↔
    a✝ ∈ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitePos_add_not_infiniteNeg {x y : ℝ*} :
    InfinitePos x → ¬InfiniteNeg y → InfinitePos (x + y)

Proof state:
x y : ℝ*
⊢ x.InfinitePos → ¬y.InfiniteNeg → (x + y).InfinitePos

Tactic:
intro hip hnin r

Result:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r : ℝ
⊢ ↑r < x + y

Proof state:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r : ℝ
⊢ ↑r < x + y

Tactic:
obtain ⟨r₂, hr₂⟩ := not_forall.mp hnin

Result:
case intro
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r < x + y

Proof state:
case h.e'_3
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r = ↑(r + -r₂) + ↑r₂

Tactic:
simp

Result:
no goals

Proof state:
case intro
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r < x + y

Tactic:
convert add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1

Result:
case h.e'_3
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r = ↑(r + -r₂) + ↑r₂
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_inf_eq_map_inf_comap [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M}
    {p' : Submodule R₂ M₂} : map f p ⊓ p' = map f (p ⊓ comap f p') :=
  le_antisymm (by rintro _ ⟨⟨x, h₁, rfl⟩, h₂⟩; exact ⟨_, ⟨h₁, h₂⟩, rfl⟩)
    (le_inf (map_mono inf_le_left) (map_le_iff_le_comap.2 inf_le_right))

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
p : Submodule R M
p' : Submodule R₂ M₂
⊢ map f p ⊓ p' ≤ map f (p ⊓ comap f p')

Tactic:
rintro _ ⟨⟨x, h₁, rfl⟩, h₂⟩

Result:
case intro.intro.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
p : Submodule R M
p' : Submodule R₂ M₂
x : M
h₁ : x ∈ ↑p
h₂ : f x ∈ ↑p'
⊢ f x ∈ map f (p ⊓ comap f p')

Proof state:
case intro.intro.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
p : Submodule R M
p' : Submodule R₂ M₂
x : M
h₁ : x ∈ ↑p
h₂ : f x ∈ ↑p'
⊢ f x ∈ map f (p ⊓ comap f p')

Tactic:
exact ⟨_, ⟨h₁, h₂⟩, rfl⟩

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive]
lemma prod_lt_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i < 1 ↔ f < 1

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : OrderedCancelCommMonoid M
f : ι → M
hf : f ≤ 1
⊢ ∏ i : ι, f i < 1 ↔ f < 1

Tactic:
obtain rfl | hf := hf.eq_or_lt <;> simp [*, prod_lt_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
/-- The special-value formula `Γ(k + 1/2) = (2 * k - 1)‼ * √π / (2 ^ k))` for half-integer
values of the gamma function in terms of `Nat.doubleFactorial`. -/
lemma Real.Gamma_nat_add_half (k : ℕ) :
    Gamma (k + 1 / 2) = (2 * k - 1 : ℕ)‼ * √π / (2 ^ k)

Proof state:
case zero

⊢ Gamma (↑0 + 1 / 2) = ↑(2 * 0 - 1)‼ * √π / 2 ^ 0

Tactic:
simp [- one_div, Gamma_one_half_eq]

Result:
no goals

Proof state:
case succ
k : ℕ
⊢ Gamma (↑(k + 1) + 1 / 2) = ↑(2 * (k + 1) - 1)‼ * √π / 2 ^ (k + 1)

Tactic:
simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k

Result:
no goals

Proof state:
k : ℕ
⊢ Gamma (↑k + 1 / 2) = ↑(2 * k - 1)‼ * √π / 2 ^ k

Tactic:
cases k with
| zero => simp [- one_div, Gamma_one_half_eq]
| succ k => simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_finset_sup' (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ) :
    ball (s.sup' H p) e r = s.inf' H fun i => ball (p i) e r

Proof state:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).ball e r = s✝.inf' hs fun i => (p i).ball e r
⊢ (p a✝).ball e r ∩ (s✝.sup' hs p).ball e r = (p a✝).ball e r ⊓ s✝.inf' hs fun i => (p i).ball e r

Tactic:
simp only [inf_eq_inter, ih]

Result:
no goals

Proof state:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).ball e r = s✝.inf' hs fun i => (p i).ball e r
⊢ ((Finset.cons a✝ s✝ h✝).sup' ⋯ p).ball e r = (Finset.cons a✝ s✝ h✝).inf' ⋯ fun i => (p i).ball e r

Tactic:
rw [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup]

Result:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).ball e r = s✝.inf' hs fun i => (p i).ball e r
⊢ (p a✝).ball e r ∩ (s✝.sup' hs p).ball e r = (p a✝).ball e r ⊓ s✝.inf' hs fun i => (p i).ball e r

Proof state:
case singleton
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
⊢ ({a✝}.sup' ⋯ p).ball e r = {a✝}.inf' ⋯ fun i => (p i).ball e r

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
⊢ (s.sup' H p).ball e r = s.inf' H fun i => (p i).ball e r

Tactic:
induction H using Finset.Nonempty.cons_induction with
| singleton => simp
| cons _ _ _ hs ih =>
  rw [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup]
  simp only [inf_eq_inter, ih]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
lemma arrowMap_functor (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) :
    arrowMap (functor hj iter) i₁ i₂ h₁₂ h₂.le =
      Arrow.mk (mapObj (iter i₁ (lt_of_le_of_lt h₁₂ h₂)) (iter i₂ h₂) h₁₂
        (by simp) (by simp) h₁₂) :=
  arrowMap_ofCocone _ _ _ _ h₂

Proof state:
C : Type u_1
inst✝⁵ : Category.{?u.30684, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ i₁ ≤ i₁

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{?u.30684, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ i₂ ≤ i₂

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero (hab : a ≤ b)
    (hfi : IntervalIntegrable f μ a b) (hgi : IntervalIntegrable g μ a b)
    (hle : f ≤ᵐ[μ.restrict (Ioc a b)] g) (hlt : μ.restrict (Ioc a b) {x | f x < g x} ≠ 0) :
    (∫ x in a..b, f x ∂μ) < ∫ x in a..b, g x ∂μ

Proof state:
case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] fun x => g x - f x

case hfi
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ Integrable (fun x => g x - f x) (μ.restrict (Ioc a b))

Tactic:
exacts [hle.mono fun x => sub_nonneg.2, hgi.1.sub hfi.1]

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 < (μ.restrict (Ioc a b)) (support fun x => g x - f x)

Tactic:
refine pos_iff_ne_zero.2 (mt (measure_mono_null ?_) hlt)

Result:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ {x | f x < g x} ⊆ support fun x => g x - f x

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ {x | f x < g x} ⊆ support fun x => g x - f x

Tactic:
exact fun x hx => (sub_pos.2 hx.out).ne'

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ ∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
  MeasureTheory.integral_pos_iff_support_of_nonneg_ae]

Result:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 < (μ.restrict (Ioc a b)) (support fun x => g x - f x)

case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] fun x => g x - f x

case hfi
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ Integrable (fun x => g x - f x) (μ.restrict (Ioc a b))
-- Mathlib/MeasureTheory/Function/LpOrder.lean
theorem coeFn_nonneg (f : Lp E p μ) : 0 ≤ᵐ[μ] f ↔ 0 ≤ f

Proof state:
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
h0 : ↑↑0 =ᶠ[ae μ] 0
h : 0 ≤ᶠ[ae μ] ↑↑f
a✝¹ : α
a✝ : 0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = 0 a✝¹
⊢ ↑↑0 a✝¹ ≤ ↑↑f a✝¹

Tactic:
rwa [h2]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
h0 : ↑↑0 =ᶠ[ae μ] 0
⊢ 0 ≤ᶠ[ae μ] ↑↑f ↔ ↑↑0 ≤ᶠ[ae μ] ↑↑f

Tactic:
constructor <;> intro h <;> filter_upwards [h, h0] with _ _ h2

Result:
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
h0 : ↑↑0 =ᶠ[ae μ] 0
h : 0 ≤ᶠ[ae μ] ↑↑f
a✝¹ : α
a✝ : 0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = 0 a✝¹
⊢ ↑↑0 a✝¹ ≤ ↑↑f a✝¹

case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
h0 : ↑↑0 =ᶠ[ae μ] 0
h : ↑↑0 ≤ᶠ[ae μ] ↑↑f
a✝¹ : α
a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = 0 a✝¹
⊢ 0 a✝¹ ≤ ↑↑f a✝¹

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
⊢ 0 ≤ᶠ[ae μ] ↑↑f ↔ ↑↑0 ≤ᶠ[ae μ] ↑↑f

Tactic:
have h0 := Lp.coeFn_zero E p μ

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
h0 : ↑↑0 =ᶠ[ae μ] 0
⊢ 0 ≤ᶠ[ae μ] ↑↑f ↔ ↑↑0 ≤ᶠ[ae μ] ↑↑f

Proof state:
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
h0 : ↑↑0 =ᶠ[ae μ] 0
h : ↑↑0 ≤ᶠ[ae μ] ↑↑f
a✝¹ : α
a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = 0 a✝¹
⊢ 0 a✝¹ ≤ ↑↑f a✝¹

Tactic:
rwa [← h2]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
⊢ 0 ≤ᶠ[ae μ] ↑↑f ↔ 0 ≤ f

Tactic:
rw [← coeFn_le]

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : ↥(Lp E p μ)
⊢ 0 ≤ᶠ[ae μ] ↑↑f ↔ ↑↑0 ≤ᶠ[ae μ] ↑↑f
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsuppLid_single_tmul_single (a : ι) (b : κ) (r : R) (n : N) :
    finsuppTensorFinsuppLid R N ι κ (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) =
      Finsupp.single (a, b) (r • n)

Proof state:
R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
a : ι
b : κ
r : R
n : N
⊢ (finsuppTensorFinsuppLid R N ι κ) (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = Finsupp.single (a, b) (r • n)

Tactic:
simp [finsuppTensorFinsuppLid]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem homogeneousSubmodule_eq_finsupp_supported (n : ℕ) :
    homogeneousSubmodule σ R n = Finsupp.supported _ R { d | d.degree = n }

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R n = supported R R {d | d.degree = n}

Tactic:
simp_rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R n = supported R R {d | (weight fun x => 1) d = n}

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R n = supported R R {d | (weight fun x => 1) d = n}

Tactic:
exact weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafIso_hom (hF : IsColimit <| F.mapCocone (coconeRightOpOfCone S.asLimitCone)) :
    (lanPresheafIso hF).hom = colimit.desc _ (LightProfinite.Extend.cocone _ _)

Proof state:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ ((colimit.isColimit (S.diagram.rightOp ⋙ F)).coconePointUniqueUpToIso hF).hom =
    colimit.desc
      (LightProfinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (Cocone.whisker (LightProfinite.Extend.functorOp S.asLimitCone) (LightProfinite.Extend.cocone F S))

Tactic:
rfl

Result:
no goals

Proof state:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F S)

Tactic:
simp [lanPresheafIso, Final.colimitIso]

Result:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ ((colimit.isColimit (S.diagram.rightOp ⋙ F)).coconePointUniqueUpToIso hF).hom =
    colimit.desc
      (LightProfinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (Cocone.whisker (LightProfinite.Extend.functorOp S.asLimitCone) (LightProfinite.Extend.cocone F S))
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_le_of_mem {m : ι} (hin : n ≤ i) (him : i ≤ m) (his : u i ω ∈ s) :
    hitting u s n m ω ≤ i

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
⊢ hitting u s n m ω ≤ i

Tactic:
have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s := ⟨i, ⟨hin, him⟩, his⟩

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ hitting u s n m ω ≤ i

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ i

Tactic:
exact csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter ⟨hin, him⟩ his)

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ hitting u s n m ω ≤ i

Tactic:
simp_rw [hitting, if_pos h_exists]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ i
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_inter_add_cRk_union_le : M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Proof state:
case intro.intro.intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨IY, hIY, hIY'⟩ :=
  hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)

Result:
case intro.intro.intro.intro.intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Proof state:
case intro.intro.intro.intro.intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (IX ∪ IY) + #↑Ii ≤ #↑(IX ∪ IY) + #↑(IX ∩ IY)

Tactic:
exact add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))

Result:
no goals

Proof state:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)

Result:
case intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Proof state:
case intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨IX, hIX, hIX'⟩ :=
  hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)

Result:
case intro.intro.intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Proof state:
case intro.intro.intro.intro.intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
  cRk_union_closure_eq, ← hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk,
  ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]

Result:
case intro.intro.intro.intro.intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (IX ∪ IY) + #↑Ii ≤ #↑(IX ∪ IY) + #↑(IX ∩ IY)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_dblXYZ (P : Fin 3 → A) : (W'.baseChange B).toJacobian.dblXYZ (f ∘ P) =
    f ∘ (W'.baseChange A).toJacobian.dblXYZ P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.dblXYZ (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toJacobian.dblXYZ P

Tactic:
rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
lemma continuous_iff_from_nat {Y : Type*} [TopologicalSpace Y] (f : OnePoint ℕ → Y) :
    Continuous f ↔ Tendsto (fun x : ℕ ↦ f x) atTop (𝓝 (f ∞))

Proof state:
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint ℕ → Y
⊢ Continuous f ↔ Tendsto (fun x => f ↑x) atTop (𝓝 (f ∞))

Tactic:
rw [continuous_iff_from_discrete, Nat.cofinite_eq_atTop]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kerase_append_right {a} :
    ∀ {l₁ l₂ : List (Sigma β)}, a ∉ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
  | [], _, _ => rfl
  | _ :: l₁, l₂, h => by
    simp only [keys_cons, mem_cons, not_or] at h
    simp [h.1, kerase_append_right h.2]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a = head✝.fst ∧ a ∉ l₁.keys
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂

Tactic:
simp [h.1, kerase_append_right h.2]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : a ∉ (head✝ :: l₁).keys
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂

Tactic:
simp only [keys_cons, mem_cons, not_or] at h

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a = head✝.fst ∧ a ∉ l₁.keys
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
-- Mathlib/Algebra/DualNumber.lean
theorem commute_eps_left [Semiring R] (x : DualNumber R) : Commute ε x

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ Commute ε x

Tactic:
ext <;> simp

Result:
no goals