harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
    enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f)

Proof state:
case nil
α : Type u_1
β : Type u_2
n : Nat
f : α → β
⊢ enumFrom n (map f []) = map (Prod.map id f) (enumFrom n [])

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
l : List α
f : α → β
⊢ enumFrom n (map f l) = map (Prod.map id f) (enumFrom n l)

Tactic:
induction l with
| nil => rfl
| cons hd tl IH =>
  rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map]
  rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
n : Nat
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ (n, f hd) :: map (Prod.map (fun x => x + 1) id ∘ Prod.map id f) (enumFrom n tl) =
    Prod.map id f (n, hd) :: map (Prod.map id f ∘ Prod.map (fun x => x + 1) id) (enumFrom n tl)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
n : Nat
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ enumFrom n (map f (hd :: tl)) = map (Prod.map id f) (enumFrom n (hd :: tl))

Tactic:
rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map]

Result:
case cons
α : Type u_1
β : Type u_2
n : Nat
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ (n, f hd) :: map (Prod.map (fun x => x + 1) id ∘ Prod.map id f) (enumFrom n tl) =
    Prod.map id f (n, hd) :: map (Prod.map id f ∘ Prod.map (fun x => x + 1) id) (enumFrom n tl)
-- Mathlib/MeasureTheory/Measure/Comap.lean
lemma comap_symm {μ : Measure α} (e : α ≃ᵐ β) : μ.comap e.symm = μ.map e

Proof state:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet (⇑e.symm '' s)

Tactic:
exact fun t ht ↦ e.symm.measurableSet_image.mpr ht

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ (Measure.comap (⇑e.symm) μ) s = (Measure.map (⇑e) μ) s

Tactic:
rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm]

Result:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet (⇑e.symm '' s)

Proof state:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measure.comap (⇑e.symm) μ = Measure.map (⇑e) μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ (Measure.comap (⇑e.symm) μ) s = (Measure.map (⇑e) μ) s
-- Mathlib/Topology/Instances/Int.lean
theorem cofinite_eq : (cofinite : Filter ℤ) = atBot ⊔ atTop

Proof state:
⊢ cofinite = atBot ⊔ atTop

Tactic:
rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem X_mem_lifts (f : R →+* S) : (X : S[X]) ∈ lifts f :=
  ⟨X, by
    simp only [coe_mapRingHom, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, map_X,
      and_self_iff]⟩

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
⊢ (mapRingHom f) X = X

Tactic:
simp only [coe_mapRingHom, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, map_X,
  and_self_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem principal_opow_omega (o : Ordinal) : Principal (· ^ ·) (ω_ o)

Proof state:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ℵ₀ < ℵ_ o

Tactic:
rwa [← aleph_zero, aleph_lt_aleph]

Result:
no goals

Proof state:
case inl

⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ 0)

Tactic:
rw [omega_zero]

Result:
case inl

⊢ Principal (fun x1 x2 => x1 ^ x2) ω

Proof state:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
hb : b < ω_ o
⊢ (fun x1 x2 => x1 ^ x2) a b < ω_ o

Tactic:
rw [lt_omega_iff_card_lt] at ha hb ⊢

Result:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 => x1 ^ x2) a b).card < ℵ_ o

Proof state:
case inl

⊢ Principal (fun x1 x2 => x1 ^ x2) ω

Tactic:
exact principal_opow_omega0

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ o)

Tactic:
obtain rfl | ho := Ordinal.eq_zero_or_pos o

Result:
case inl

⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ 0)

case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ o)

Proof state:
case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ o)

Tactic:
intro a b ha hb

Result:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
hb : b < ω_ o
⊢ (fun x1 x2 => x1 ^ x2) a b < ω_ o

Proof state:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 => x1 ^ x2) a b).card < ℵ_ o

Tactic:
apply (card_opow_le a b).trans_lt (max_lt _ (max_lt ha hb))

Result:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ℵ₀ < ℵ_ o
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
/-- If an integrable function has zero integral on all closed sets, then it is zero
almost everywhere. -/
lemma ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero {μ : Measure β} {f : β → E}
    (hf : Integrable f μ) (h'f : ∀ (s : Set β), IsClosed s → ∫ x in s, f x ∂μ = 0) :
    f =ᵐ[μ] 0

Proof state:
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed s → ∫ (x : β) in s, f x ∂μ = 0
⊢ ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0

Tactic:
intro t t_meas ht

Result:
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed s → ∫ (x : β) in s, f x ∂μ = 0
t : Set β
t_meas : MeasurableSet t
ht : ∫ (x : β) in t, f x ∂μ = 0
⊢ ∫ (x : β) in tᶜ, f x ∂μ = 0

Proof state:
case iUnion
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed s → ∫ (x : β) in s, f x ∂μ = 0
A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0
s : Set β
g : ℕ → Set β
g_disj : Pairwise (Function.onFun Disjoint g)
g_meas : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), ∫ (x : β) in g i, f x ∂μ = 0
⊢ ∫ (x : β) in ⋃ i, g i, f x ∂μ = 0

Tactic:
simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_one_iff : s.encard ≤ 1 ↔ ∀ a b, a ∈ s → b ∈ s → a = b

Proof state:
α : Type u_1
s : Set α
h : s.Nonempty → ∃ x, s = {x}
a b : α
has : a ∈ s
hbs : b ∈ s
⊢ a = b

Tactic:
obtain ⟨x, rfl⟩ := h ⟨_, has⟩

Result:
case intro
α : Type u_1
a b x : α
h : {x}.Nonempty → ∃ x_1, {x} = {x_1}
has : a ∈ {x}
hbs : b ∈ {x}
⊢ a = b

Proof state:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
rw [encard_le_one_iff_eq, or_iff_not_imp_left, ← Ne, ← nonempty_iff_ne_empty]

Result:
α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Proof state:
α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
refine ⟨fun h a b has hbs ↦ ?_,
  fun h ⟨x, hx⟩ ↦ ⟨x, ((singleton_subset_iff.2 hx).antisymm' (fun y hy ↦ h _ _ hy hx))⟩⟩

Result:
α : Type u_1
s : Set α
h : s.Nonempty → ∃ x, s = {x}
a b : α
has : a ∈ s
hbs : b ∈ s
⊢ a = b

Proof state:
case intro
α : Type u_1
a b x : α
h : {x}.Nonempty → ∃ x_1, {x} = {x_1}
has : a ∈ {x}
hbs : b ∈ {x}
⊢ a = b

Tactic:
rw [(has : a = x), (hbs : b = x)]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv i (X j : MvPolynomial σ R) = 0

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ (pderiv i) (X j) = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ (pderiv i) (X j) = 0

Tactic:
classical simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem exists_of_findSome?_eq_some {f : α → Option β} {l : Vector α n} (w : l.findSome? f = some b) :
    ∃ a, a ∈ l ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
n : Nat
b : β
f : α → Option β
l : Vector α n
w : findSome? f l = some b
⊢ ∃ a, a ∈ l ∧ f a = some b

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
b : β
f : α → Option β
l : Array α
w : findSome? f { toArray := l, size_toArray := ⋯ } = some b
⊢ ∃ a, a ∈ { toArray := l, size_toArray := ⋯ } ∧ f a = some b

Proof state:
case mk
α : Type u_1
β : Type u_2
b : β
f : α → Option β
l : Array α
w : findSome? f { toArray := l, size_toArray := ⋯ } = some b
⊢ ∃ a, a ∈ { toArray := l, size_toArray := ⋯ } ∧ f a = some b

Tactic:
simpa using Array.exists_of_findSome?_eq_some (by simpa using w)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
f : α → Option β
l : Array α
w : findSome? f { toArray := l, size_toArray := ⋯ } = some b
⊢ Array.findSome? f l = some b

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem mulVec_cons {α} [CommSemiring α] (A : m' → Fin n.succ → α) (x : α) (v : Fin n → α) :
    (of A) *ᵥ (vecCons x v) = x • vecHead ∘ A + (of (vecTail ∘ A)) *ᵥ v

Proof state:
n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
⊢ of A *ᵥ vecCons x v = x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v

Tactic:
ext i

Result:
case h
n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
i : m'
⊢ (of A *ᵥ vecCons x v) i = (x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v) i

Proof state:
case h
n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
i : m'
⊢ (of A *ᵥ vecCons x v) i = (x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v) i

Tactic:
simp [mulVec, mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem vec_ex1_dioph (n) {S : Set (Vector3 ℕ (succ n))} (d : Dioph S) :
    Dioph {v : Fin2 n → ℕ | ∃ x, (x::v) ∈ S} :=
  ext (ex1_dioph <| reindex_dioph _ (none::some) d) fun v =>
    exists_congr fun x => by
      dsimp
      rw [show Option.elim' x v ∘ cons none some = x::v from
          funext fun s => by rcases s with a | b <;> rfl]

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ x ::ₒ v ∈ {v | (v ∘ none :: some) ∈ S} ↔ (x :: v) ∈ S

Tactic:
dsimp

Result:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
s : Fin2 (n + 1)
⊢ ((x ::ₒ v) ∘ none :: some) s = (x :: v) s

Tactic:
rcases s with a | b <;> rfl

Result:
no goals

Proof state:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S

Tactic:
rw [show Option.elim' x v ∘ cons none some = x::v from
    funext fun s => by rcases s with a | b <;> rfl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem exp_log (hx : 0 < x) : exp (log x) = x

Proof state:
x : ℝ
hx : 0 < x
⊢ rexp (log x) = x

Tactic:
rw [exp_log_eq_abs hx.ne']

Result:
x : ℝ
hx : 0 < x
⊢ |x| = x

Proof state:
x : ℝ
hx : 0 < x
⊢ |x| = x

Tactic:
exact abs_of_pos hx

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_eq_zero [Nontrivial E] (n : ℕ) : ofScalars E c n = 0 ↔ c n = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ∃ x, ¬(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x = 0 x

Tactic:
use fun _ ↦ 1

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ¬((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 1) = 0 fun x => 1

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ¬((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 1) = 0 fun x => 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ofScalars E c n = 0 ↔ c n = 0

Tactic:
rw [ofScalars, smul_eq_zero (c := c n) (x := ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ c n = 0 ∨ ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E = 0 ↔ c n = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ c n = 0 ∨ ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E = 0 ↔ c n = 0

Tactic:
refine or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
n : ℕ
⊢ ∃ x, ¬(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x = 0 x
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.zsmul [AddGroup α] (h : Periodic f c) (n : ℤ) : Periodic f (n • c)

Proof state:
case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)

Tactic:
simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℤ
⊢ Periodic f (n • c)

Tactic:
rcases n with n | n

Result:
case ofNat
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)

Proof state:
case ofNat
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

Tactic:
simpa only [Int.ofNat_eq_coe, natCast_zsmul] using h.nsmul n

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
lemma two_mul_le_add_of_sq_eq_mul [ExistsAddOfLE α] [MulPosStrictMono α] [PosMulStrictMono α]
    [AddLeftReflectLE α] [AddLeftMono α] {a b r : α}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) : 2 * r ≤ a + b

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)

Tactic:
conv_rhs => rw [← pow_two]

Result:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r * (2 * r) ≤ (a + b) ^ 2

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r ≤ a + b

Tactic:
apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)

Result:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r * (2 * r) ≤ (a + b) ^ 2

Tactic:
convert four_mul_le_sq_add a b using 1

Result:
case h.e'_3
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r * (2 * r) = 4 * a * b

Proof state:
case h.e'_3
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b r : α
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 = a * b
⊢ 2 * r * (2 * r) = 4 * a * b

Tactic:
rw [mul_mul_mul_comm, two_mul, two_add_two_eq_four, ← pow_two, ht, mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_eq_eraseP' (a : α) (l : Array α) : l.erase a = l.eraseP (· == a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ { toList := l }.erase a = { toList := l }.eraseP fun x => x == a

Tactic:
simp [List.erase_eq_eraseP']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ l.erase a = l.eraseP fun x => x == a

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ { toList := l }.erase a = { toList := l }.eraseP fun x => x == a
-- Mathlib/Data/ENat/Lattice.lean
lemma biSup_add_biSup_le' {p : ι → Prop} {q : κ → Prop} (hp : ∃ i, p i) (hq : ∃ j, q j)
    {g : κ → ℕ∞} (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) :
    (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a

Proof state:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Result:
no goals

Proof state:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]

Result:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a
-- Mathlib/Order/Hom/Bounded.lean
theorem map_eq_bot_iff [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β]
    (f : F) {a : α} : f a = ⊥ ↔ a = ⊥

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ f a = ⊥ ↔ a = ⊥

Tactic:
letI : BotHomClass F α β := OrderIsoClass.toBotHomClass

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : BotHomClass F α β := OrderIsoClass.toBotHomClass
⊢ f a = ⊥ ↔ a = ⊥

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : BotHomClass F α β := OrderIsoClass.toBotHomClass
⊢ f a = ⊥ ↔ a = ⊥

Tactic:
rw [← map_bot f, (EquivLike.injective f).eq_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem adj_congr_of_sym2 {u v w x : V} (h : s(u, v) = s(w, x)) : G.Adj u v ↔ G.Adj w x

Proof state:
case inl
V : Type u
G : SimpleGraph V
u v w x : V
hl : u = w ∧ v = x
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
rw [hl.1, hl.2]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
h : s(u, v) = s(w, x)
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h

Result:
V : Type u
G : SimpleGraph V
u v w x : V
h : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x

Proof state:
case inr
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
rw [hr.1, hr.2, adj_comm]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
h : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
rcases h with hl | hr

Result:
case inl
V : Type u
G : SimpleGraph V
u v w x : V
hl : u = w ∧ v = x
⊢ G.Adj u v ↔ G.Adj w x

case inr
V : Type u
G : SimpleGraph V
u v w x : V
hr : u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_singleton : (∏ᶠ i ∈ ({a} : Set α), f i) = f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a

Tactic:
rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem perm_orderedInsert (a) : ∀ l : List α, orderedInsert r a l ~ a :: l
  | [] => Perm.refl _
  | b :: l => by
    by_cases h : a ≼ b
    · simp [orderedInsert, h]
    · simpa [orderedInsert, h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simpa [orderedInsert, h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

Result:
no goals

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simp [orderedInsert, h]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
by_cases h : a ≼ b

Result:
case pos
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

case neg
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
lemma LocallyLipschitzOn.mono (hf : LocallyLipschitzOn t f) (h : s ⊆ t) : LocallyLipschitzOn s f :=
  fun x hx ↦ by obtain ⟨K, u, hu, hfu⟩ := hf (h hx); exact ⟨K, u, nhdsWithin_mono _ h hu, hfu⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
obtain ⟨K, u, hu, hfu⟩ := hf (h hx)

Result:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
exact ⟨K, u, nhdsWithin_mono _ h hu, hfu⟩

Result:
no goals