harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem atTop_Ioi_eq [Preorder α] [IsDirected α (· ≤ ·)] (a : α) :
    atTop = comap ((↑) : Ioi a → α) atTop

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
⊢ atTop = comap Subtype.val atTop

Tactic:
rcases isEmpty_or_nonempty (Ioi a) with h|⟨⟨b, hb⟩⟩

Result:
case inl
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
h : IsEmpty ↑(Ioi a)
⊢ atTop = comap Subtype.val atTop

case inr.intro.mk
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop

Proof state:
case inl
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
h : IsEmpty ↑(Ioi a)
⊢ atTop = comap Subtype.val atTop

Tactic:
subsingleton

Result:
no goals

Proof state:
case inr.intro.mk
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop

Tactic:
rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : Set (Sigma σ)) :
    ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s

Proof state:
case h.mp.intro.intro.intro
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
i : ι
a : σ i
h : ⟨i, a⟩ ∈ s
⊢ ⟨i, a⟩ ∈ s

Tactic:
exact h

Result:
no goals

Proof state:
case h
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) ↔ x ∈ s

Tactic:
constructor

Result:
case h.mp
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) → x ∈ s

case h.mpr
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ s → ∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x

Proof state:
case h.mpr.mk
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
i : ι
a : σ i
h : ⟨i, a⟩ ∈ s
⊢ ∃ i_1 x, ⟨i_1, x⟩ ∈ s ∧ ⟨i_1, x⟩ = ⟨i, a⟩

Tactic:
exact ⟨i, a, h, rfl⟩

Result:
no goals

Proof state:
case h.mpr
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
h : x ∈ s
⊢ ∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x

Tactic:
obtain ⟨i, a⟩ := x

Result:
case h.mpr.mk
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
i : ι
a : σ i
h : ⟨i, a⟩ ∈ s
⊢ ∃ i_1 x, ⟨i_1, x⟩ ∈ s ∧ ⟨i_1, x⟩ = ⟨i, a⟩

Proof state:
case h.mp
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) → x ∈ s

Tactic:
rintro ⟨i, a, h, rfl⟩

Result:
case h.mp.intro.intro.intro
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
i : ι
a : σ i
h : ⟨i, a⟩ ∈ s
⊢ ⟨i, a⟩ ∈ s

Proof state:
case h
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) ↔ x ∈ s

Tactic:
simp only [mem_iUnion, mem_image, mem_preimage]

Result:
case h
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) ↔ x ∈ s

Proof state:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
⊢ ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s

Tactic:
ext x

Result:
case h
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) ↔ x ∈ s

Proof state:
case h.mpr
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ s → ∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x

Tactic:
intro h

Result:
case h.mpr
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
h : x ∈ s
⊢ ∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem back?_map {f : α → β} {l : Vector α n} : (l.map f).back? = l.back?.map f

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).back? =
    Option.map f { toArray := toArray✝, size_toArray := size_toArray✝ }.back?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
⊢ (map f l).back? = Option.map f l.back?

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).back? =
    Option.map f { toArray := toArray✝, size_toArray := size_toArray✝ }.back?
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem mem_of_subset_of_mem (h : x.IsOrdinal) (hz : z.IsOrdinal) (hx : x ⊆ y) (hy : y ∈ z) :
    x ∈ z

Proof state:
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ y
hy : y ∈ z
⊢ x ∈ z

Tactic:
obtain rfl | hx := h.eq_or_mem_of_subset (hz.mem hy) hx

Result:
case inl
x z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ x
hy : x ∈ z
⊢ x ∈ z

case inr
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx✝ : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z

Proof state:
case inl
x z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx : x ⊆ x
hy : x ∈ z
⊢ x ∈ z

Tactic:
exact hy

Result:
no goals

Proof state:
case inr
x y z : ZFSet.{u}
h : x.IsOrdinal
hz : z.IsOrdinal
hx✝ : x ⊆ y
hy : y ∈ z
hx : x ∈ y
⊢ x ∈ z

Tactic:
exact hz.mem_trans hx hy

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mrangeRestrict_mker (f : M →* N) : mker (mrangeRestrict f) = mker f

Proof state:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ x ∈ mker f.mrangeRestrict ↔ x ∈ mker f

Tactic:
change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1

Result:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ ⟨f x, ⋯⟩ = ⟨1, ⋯⟩ ↔ f x = 1

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
⊢ mker f.mrangeRestrict = mker f

Tactic:
ext x

Result:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ x ∈ mker f.mrangeRestrict ↔ x ∈ mker f

Proof state:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ ⟨f x, ⋯⟩ = ⟨1, ⋯⟩ ↔ f x = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_none_of_filterMap_eq_nil (h : filterMap f xs = []) : ∀ x ∈ xs, f x = none

Proof state:
case cons.h_1.head
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
h : filterMap f ys = []
heq✝ : f x = none
⊢ f x = none

Tactic:
assumption

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : filterMap f xs = []
⊢ ∀ (x : α✝¹), x ∈ xs → f x = none

Tactic:
intro x hx

Result:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : filterMap f xs = []
x : α✝¹
hx : x ∈ xs
⊢ f x = none

Proof state:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
h : filterMap f (y :: ys) = []
hx : x ∈ y :: ys
⊢ f x = none

Tactic:
simp only [filterMap_cons] at h

Result:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
h :
  (match f y with
    | none => filterMap f ys
    | some b => b :: filterMap f ys) =
    []
hx : x ∈ y :: ys
⊢ f x = none

Proof state:
case cons.h_1.tail
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
heq✝ : f y = none
h : filterMap f ys = []
hmem : Mem x ys
⊢ f x = none

Tactic:
exact ih h hmem

Result:
no goals

Proof state:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : filterMap f ys = []
⊢ f x = none

Tactic:
cases hx with
| head => assumption
| tail _ hmem => exact ih h hmem

Result:
no goals

Proof state:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: filterMap f ys = []
⊢ f x = none

Tactic:
contradiction

Result:
no goals

Proof state:
case nil
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
h : filterMap f [] = []
hx : x ∈ []
⊢ f x = none

Tactic:
contradiction

Result:
no goals

Proof state:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
h :
  (match f y with
    | none => filterMap f ys
    | some b => b :: filterMap f ys) =
    []
hx : x ∈ y :: ys
⊢ f x = none

Tactic:
split at h

Result:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
heq✝ : f y = none
h : filterMap f ys = []
⊢ f x = none

case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x y : α✝¹
ys : List α✝¹
ih : filterMap f ys = [] → x ∈ ys → f x = none
hx : x ∈ y :: ys
x✝ : Option α✝
b✝ : α✝
heq✝ : f y = some b✝
h : b✝ :: filterMap f ys = []
⊢ f x = none
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem StrictConvexSpace.of_strictConvex_unitClosedBall [LinearMap.CompatibleSMul E E 𝕜 ℝ]
    (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) : StrictConvexSpace 𝕜 E :=
  ⟨fun r hr => by simpa only [smul_unitClosedBall_of_nonneg hr.le] using h.smul r⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 ℝ
h : StrictConvex 𝕜 (closedBall 0 1)
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall 0 r)

Tactic:
simpa only [smul_unitClosedBall_of_nonneg hr.le] using h.smul r

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem archimedean_iff_nat_lt : Archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
  ⟨@exists_nat_gt α _, fun H =>
    ⟨fun x y y0 =>
      (H (x / y)).imp fun n h => le_of_lt <| by rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h⟩⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
H : ∀ (x : α), ∃ n, x < ↑n
x y : α
y0 : 0 < y
n : ℕ
h : x / y < ↑n
⊢ x < n • y

Tactic:
rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_mk {xs : Array α} {h : xs.size = n} :
    (mk xs h).attach = mk (xs.attachWith (· ∈ mk xs h) (by simp)) (by simpa using h)

Proof state:
α : Type ?u.1866
n : Nat
xs : Array α
h : xs.size = n
⊢ ∀ (x : α), x ∈ xs → (fun x => x ∈ { toArray := xs, size_toArray := h }) x

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.1866
n : Nat
xs : Array α
h : xs.size = n
⊢ (xs.attachWith (fun x => x ∈ { toArray := xs, size_toArray := h }) ⋯).size = n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Array α
h : xs.size = n
⊢ { toArray := xs, size_toArray := h }.attach =
    { toArray := xs.attachWith (fun x => x ∈ { toArray := xs, size_toArray := h }) ⋯, size_toArray := ⋯ }

Tactic:
simp [attach]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem lsum_comp_lsingle (f : α → M →ₗ[R] N) (i : α) :
    Finsupp.lsum S f ∘ₗ lsingle i = f i

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
f : α → M →ₗ[R] N
i : α
⊢ (lsum S) f ∘ₗ lsingle i = f i

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
f : α → M →ₗ[R] N
i : α
x✝ : M
⊢ ((lsum S) f ∘ₗ lsingle i) x✝ = (f i) x✝

Proof state:
case h
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
f : α → M →ₗ[R] N
i : α
x✝ : M
⊢ ((lsum S) f ∘ₗ lsingle i) x✝ = (f i) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem coeff_eq_zero_of_natDegree_lt {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
    p.coeff n = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n

Tactic:
exact WithBot.bot_lt_coe n

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Tactic:
rwa [degree_eq_natDegree hp, Nat.cast_lt]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
⊢ p.degree < ↑n

Tactic:
subst hp

Result:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n

Proof state:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.degree < ↑n

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
⊢ p.degree < ↑n

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.coeff n = 0

Tactic:
apply coeff_eq_zero_of_degree_lt

Result:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.degree < ↑n
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0∞) (hp1 : 1 ≤ p) : a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
rw [h_top]

Result:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ ⊤

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
have hp_pos : 0 < p := by positivity

Result:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
case neg.intro.intro
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ⊤
a : ℝ≥0
h_top : ¬↑a + b = ⊤
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p

Tactic:
lift b to ℝ≥0 using hb_top

Result:
case neg.intro.intro.intro
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬↑a + ↑b = ⊤
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p

Proof state:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top

Result:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p

Tactic:
positivity

Result:
no goals

Proof state:
case neg.intro
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
ha_top : a ≠ ⊤
hb_top : b ≠ ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
lift a to ℝ≥0 using ha_top

Result:
case neg.intro.intro
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ⊤
a : ℝ≥0
h_top : ¬↑a + b = ⊤
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p

Proof state:
case neg.intro.intro.intro
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬↑a + ↑b = ⊤
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg _ hp_pos.le] using
  ENNReal.coe_le_coe.2 (NNReal.add_rpow_le_rpow_add a b hp1)

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
by_cases h_top : a + b = ⊤

Result:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

case neg
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
case neg
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top

Result:
case neg.intro
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
ha_top : a ≠ ⊤
hb_top : b ≠ ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
    dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖(2 : 𝕜)‖

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖

Tactic:
rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / ‖2‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / ‖2‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖

Tactic:
exact div_le_div_of_nonneg_right (norm_add_le _ _) (norm_nonneg _)

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B]
    {S : Subalgebra A B} {x : B} (int : IsIntegral S x) : 2 ≤ (minpoly S x).natDegree ↔ x ∉ S

Proof state:
A : Type u_1
inst✝³ : CommRing A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
⊢ x ∈ (algebraMap (↥S) B).range ↔ x ∈ S

Tactic:
apply Set.ext_iff.mp Subtype.range_val_subtype

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : CommRing A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
⊢ 2 ≤ (minpoly (↥S) x).natDegree ↔ x ∉ S

Tactic:
rw [two_le_natDegree_iff int, Iff.not]

Result:
A : Type u_1
inst✝³ : CommRing A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
⊢ x ∈ (algebraMap (↥S) B).range ↔ x ∈ S
-- Mathlib/Algebra/Group/End.lean
theorem zpow_aux (hf : ∀ x, p x ↔ p (f x)) : ∀ {n : ℤ} (x), p x ↔ p ((f ^ n) x)
  | Int.ofNat _ => pow_aux hf
  | Int.negSucc n => by
    rw [zpow_negSucc]
    exact inv_aux.1 (pow_aux hf)

Proof state:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p ((f ^ Int.negSucc n) x)

Tactic:
rw [zpow_negSucc]

Result:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p ((f ^ (n + 1))⁻¹ x)

Proof state:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p ((f ^ (n + 1))⁻¹ x)

Tactic:
exact inv_aux.1 (pow_aux hf)

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem Units.isUnit_mul_units [Monoid M] (a : M) (u : Mˣ) : IsUnit (a * u) ↔ IsUnit a :=
  Iff.intro
    (fun ⟨v, hv⟩ => by
      have : IsUnit (a * ↑u * ↑u⁻¹)

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit (a * ↑u * ↑u⁻¹)

Tactic:
exists v * u⁻¹

Result:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑(v * u⁻¹) = a * ↑u * ↑u⁻¹

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * ↑u * ↑u⁻¹)
⊢ IsUnit a

Tactic:
rwa [mul_assoc, Units.mul_inv, mul_one] at this

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ ↑(v * u⁻¹) = a * ↑u * ↑u⁻¹

Tactic:
rw [← hv, Units.val_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit a

Tactic:
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]

Result:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * ↑u * ↑u⁻¹)
⊢ IsUnit a
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem isReal_iff {w : InfinitePlace K} :
    IsReal w ↔ ComplexEmbedding.IsReal (embedding w)

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal → ComplexEmbedding.IsReal w.embedding

Tactic:
rintro ⟨φ, ⟨hφ, rfl⟩⟩

Result:
case intro.intro
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal (mk φ).embedding

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

Tactic:
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩

Result:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal → ComplexEmbedding.IsReal w.embedding

Proof state:
case intro.intro
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
rwa [embedding_mk_eq_of_isReal hφ]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem isComplement_singleton_left {g : G} : IsComplement {g} S ↔ S = univ

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ IsComplement {g} S ↔ S = univ

Tactic:
refine
  ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => (congr_arg _ h).mpr isComplement_singleton_univ⟩

Result:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement {g} S
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S

Proof state:
case intro.mk.mk.mk
G : Type u_1
inst✝ : Group G
S : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x => ↑x.1 * ↑x.2) (⟨z, ⋯⟩, ⟨y, property✝⟩) = z * x
⊢ x ∈ S

Tactic:
rwa [← mul_left_cancel hy]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement {g} S
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S

Tactic:
obtain ⟨⟨⟨z, rfl : z = g⟩, y, _⟩, hy⟩ := h.2 (g * x)

Result:
case intro.mk.mk.mk
G : Type u_1
inst✝ : Group G
S : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x => ↑x.1 * ↑x.2) (⟨z, ⋯⟩, ⟨y, property✝⟩) = z * x
⊢ x ∈ S