harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_replace (l : List α) (a b : α) :
    (l.replace a b).head? = match l.head? with
      | none => none
      | some x => some (if a == x then b else x)

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
⊢ (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b).head? =
    some (if (a == x) = true then b else x)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a b : α
⊢ (l.replace a b).head? =
    match l.head? with
    | none => none
    | some x => some (if (a == x) = true then b else x)

Tactic:
cases l with
| nil => rfl
| cons x xs =>
  simp [replace_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
⊢ ((x :: xs).replace a b).head? =
    match (x :: xs).head? with
    | none => none
    | some x => some (if (a == x) = true then b else x)

Tactic:
simp [replace_cons]

Result:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
⊢ (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b).head? =
    some (if (a == x) = true then b else x)

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a b : α
⊢ ([].replace a b).head? =
    match [].head? with
    | none => none
    | some x => some (if (a == x) = true then b else x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x - y) x = Real.arctan (‖y‖ / ‖x‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle x (x - y) = ↑(Real.arctan (‖y‖ / ‖x‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle x (x - y) = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
exact (-o).oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem min'_lt_max'_of_card (h₂ : 1 < card s) :
    s.min' (Finset.card_pos.1 <| by omega) < s.max' (Finset.card_pos.1 <| by omega)

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
exact s.min'_lt_max' ha hb hab

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ s.min' ⋯ < s.max' ⋯

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
h₂ : 1 < #s
⊢ 0 < #s

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Iio (e : α ≃o β) (b : β) : e ⁻¹' Iio b = Iio (e.symm b)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iio b ↔ x ∈ Iio (e.symm b)

Tactic:
simp [← e.lt_iff_lt]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Iio b = Iio (e.symm b)

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iio b ↔ x ∈ Iio (e.symm b)
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_eval_one (n : ℤ) : (U R n).eval 1 = n + 1

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 1 (U R ↑n) = ↑↑n + 1
⊢ 2 * (↑n + 1 + 1) - (↑n + 1) = ↑n + 2 + 1

Tactic:
ring

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ eval 1 (U R 1) = ↑1 + 1

Tactic:
simp

Result:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 1 (U R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ 2 * (-↑n + 1) - (-↑n + 1 + 1) = -↑n

Tactic:
ring

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 1 (U R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ eval 1 (U R (-↑n - 1)) = ↑(-↑n - 1) + 1

Tactic:
simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
  ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
  sub_add_cancel]

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 1 (U R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ 2 * (-↑n + 1) - (-↑n + 1 + 1) = -↑n

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 1 (U R ↑n) = ↑↑n + 1
⊢ eval 1 (U R (↑n + 2)) = ↑(↑n + 2) + 1

Tactic:
simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
  Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (U R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 1 (U R ↑n) = ↑↑n + 1
⊢ 2 * (↑n + 1 + 1) - (↑n + 1) = ↑n + 2 + 1

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 1 (U R 0) = ↑0 + 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 1 (U R n) = ↑n + 1

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp; norm_num
| add_two n ih1 ih2 =>
  simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
    Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
  ring
| neg_add_one n ih1 ih2 =>
  simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
    ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
    sub_add_cancel]
  ring

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/TotallyDisconnected.lean
@[to_additive]
lemma exists_openSubgroup_separating {a b : G} (h : a ≠ b) :
    ∃ V : OpenSubgroup G, Disjoint (a • (V : Set G)) (b • V)

Proof state:
case h.intro
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ ↑V
hsb : b⁻¹ * s ∈ ↑V
⊢ False

Tactic:
refine dis.subset_compl_right mem_u (hV ?_)

Result:
case h.intro
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ ↑V
hsb : b⁻¹ * s ∈ ↑V
⊢ a⁻¹ * b ∈ ↑V

Proof state:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
⊢ x = ∅

Tactic:
by_contra! con

Result:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
con : x.Nonempty
⊢ False
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem monomial_zero_eq_C_apply (a : R) : monomial R 0 a = C R a

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (monomial R 0) a = (C R) a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
@[simp]
lemma algebraTensorAlgEquiv_tmul (a : A) (p : MvPolynomial σ R) :
    algebraTensorAlgEquiv R A (a ⊗ₜ p) = a • MvPolynomial.map (algebraMap R A) p

Proof state:
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
p : MvPolynomial σ R
⊢ (Algebra.ofId A (MvPolynomial σ A)) a * eval₂ (C.comp ↑(Algebra.ofId R A)) X p = C a * (map (algebraMap R A)) p

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
p : MvPolynomial σ R
⊢ (algebraTensorAlgEquiv R A) (a ⊗ₜ[R] p) = a • (map (algebraMap R A)) p

Tactic:
simp [algebraTensorAlgEquiv, Algebra.smul_def]

Result:
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
p : MvPolynomial σ R
⊢ (Algebra.ofId A (MvPolynomial σ A)) a * eval₂ (C.comp ↑(Algebra.ofId R A)) X p = C a * (map (algebraMap R A)) p
-- Mathlib/Data/List/Cycle.lean
theorem nontrivial_coe_nodup_iff {l : List α} (hl : l.Nodup) :
    Nontrivial (l : Cycle α) ↔ 2 ≤ l.length

Proof state:
case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)

Tactic:
refine ⟨hd, hd', ?_, by simp⟩

Result:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ¬hd = hd'

Proof state:
α : Type u_1
l : List α
hl : l.Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ l.length

Tactic:
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)

Result:
case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length

case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Proof state:
α : Type u_1
l : List α
hl : l.Nodup
⊢ (↑l).Nontrivial ↔ 2 ≤ l.length

Tactic:
rw [Nontrivial]

Result:
α : Type u_1
l : List α
hl : l.Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ l.length

Proof state:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ¬hd = hd'

Tactic:
simp only [not_or, mem_cons, nodup_cons] at hl

Result:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup
⊢ ¬hd = hd'

Proof state:
case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
simp only [mem_cons, exists_prop, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
  Nat.zero_le, iff_true]

Result:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)

Proof state:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup
⊢ ¬hd = hd'

Tactic:
exact hl.left.left

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem zero_add (a : Nimber) : 0 + a = a

Proof state:
a : Nimber
⊢ 0 + a = a

Tactic:
rw [Nimber.add_comm, Nimber.add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
    (hnm : n < m) : drop m (l.set n a) = l.drop m :=
  ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)

Proof state:
α : Type u_1
a : α
n m : Nat
l : List α
hnm : n < m
k : Nat
⊢ n ≠ m + k

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a : α
n m : Nat
l : List α
hnm : n < m
k : Nat
⊢ (drop m (l.set n a))[k]? = (drop m l)[k]?

Tactic:
simpa only [getElem?_drop] using getElem?_set_ne (by omega)

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
/-- Useful for replacing `f` by `Spec.map φ` everywhere in proofs. -/
lemma Spec.map_surjective {R S : CommRingCat} :
    Function.Surjective (Spec.map : (R ⟶ S) → _)

Proof state:
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ ∃ a, map a = f

Tactic:
use Spec.preimage f

Result:
case h
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ map (preimage f) = f

Proof state:
case h
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ map (preimage f) = f

Tactic:
simp

Result:
no goals

Proof state:
R S : CommRingCat
⊢ Function.Surjective map

Tactic:
intro f

Result:
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ ∃ a, map a = f
-- Mathlib/Data/Set/MemPartition.lean
lemma mem_memPartitionSet (f : ℕ → Set α) (n : ℕ) (a : α) : a ∈ memPartitionSet f n a

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
a : α
⊢ a ∈ memPartitionSet f 0 a

Tactic:
simp [memPartitionSet]

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ memPartitionSet f (n + 1) a

Tactic:
rw [memPartitionSet_succ]

Result:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
split_ifs with h <;> exact ⟨ih, h⟩

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
⊢ a ∈ memPartitionSet f n a

Tactic:
induction n with
| zero => simp [memPartitionSet]
| succ n ih =>
  classical
  rw [memPartitionSet_succ]
  split_ifs with h <;> exact ⟨ih, h⟩

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ memPartitionSet f (n + 1) a

Tactic:
classical
rw [memPartitionSet_succ]
split_ifs with h <;> exact ⟨ih, h⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem unifTight_iff_ennreal {_ : MeasurableSpace α} (f : ι → α → β) (p : ℝ≥0∞) (μ : Measure α) :
    UnifTight f p μ ↔ ∀ ⦃ε : ℝ≥0∞⦄, 0 < ε → ∃ s : Set α,
      μ s ≠ ∞ ∧ ∀ i, eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ 0 < ⊤ → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ⊤

Tactic:
simp only [zero_lt_top, le_top, implies_true, and_true, true_implies]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ ∃ s, μ s ≠ ⊤

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ μ ∅ ≠ ⊤

Tactic:
simpa only [measure_empty] using zero_ne_top

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔
    (∀ (r : ℝ≥0), 0 < r → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑r) ∧
      (0 < ⊤ → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ⊤)

Tactic:
refine (and_iff_left ?_).symm

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ 0 < ⊤ → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ⊤

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ ∃ s, μ s ≠ ⊤

Tactic:
use ∅

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ μ ∅ ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔ ∀ ⦃ε : ℝ≥0∞⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε

Tactic:
simp only [ENNReal.forall_ennreal, ENNReal.coe_pos]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔
    (∀ (r : ℝ≥0), 0 < r → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑r) ∧
      (0 < ⊤ → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ⊤)
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_ite_zero (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
    𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (𝔼 i : ι, if p i then a else 0) = if ∃ i, p i then (↑(card ι))⁻¹ • a else 0

Tactic:
simp [univ.expect_ite_zero p (by simpa using h)]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
lemma div_neg (a : R) : a / -b = -(a / b)

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
b a : R
⊢ a / -b = -(a / b)

Tactic:
rw [← div_neg_eq_neg_div]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem prod_le_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
    s.prod t ≤ u ↔ s.map (inl M N) ≤ u ∧ t.map (inr M N) ≤ u

Proof state:
case a
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (inr M N) x2 ∈ map (inr M N) t

Tactic:
simpa using h2

Result:
no goals
-- Mathlib/Algebra/Order/Group/Indicator.lean
@[to_additive]
lemma iSup_mulIndicator {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f : ι → α → M}
    {s : ι → Set α} (h1 : (⊥ : M) = 1) (hf : Monotone f) (hs : Monotone s) :
    ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)

Proof state:
case pos.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j : ι
⊢ f j a ≤ ⨆ i, (s i).mulIndicator (f i) a

Tactic:
obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j

Result:
case pos.intro.intro.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f j a ≤ ⨆ i, (s i).mulIndicator (f i) a
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem pow_mul_apply_eq_pow_mul {M : Type*} [Monoid M] (f : M₀ → M) {x : M₀}
    (hx : ∀ y : M₀, f (x * y) = f x * f y) (n : ℕ) :
    ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y

Proof state:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

Result:
no goals

Proof state:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
⊢ ∀ (y : M₀), f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
intro y

Result:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Proof state:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (x ^ 0 * y) = f x ^ 0 * f y

Tactic:
rw [pow_zero, pow_zero, one_mul, one_mul]

Result:
no goals

Proof state:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
⊢ ∀ (y : M₀), f (x ^ 0 * y) = f x ^ 0 * f y

Tactic:
intro y

Result:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (x ^ 0 * y) = f x ^ 0 * f y

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y

Tactic:
induction n with
| zero => intro y; rw [pow_zero, pow_zero, one_mul, one_mul]
| succ n hn => intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail?_append_of_ne_nil {l l' : List α} (_ : l ≠ []) : (l ++ l').tail? = some (l.tail ++ l') :=
  match l with
  | _ :: _ => by simp

Proof state:
α : Type u_1
l l' : List α
head✝ : α
tail✝ : List α
x✝ : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ l').tail? = some ((head✝ :: tail✝).tail ++ l')

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_self (s : Finset α) : powersetCard s.card s = {s}

Proof state:
case h.mpr
α : Type u_1
a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ #a✝ = #a✝

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s ↔ a✝ = s

Tactic:
constructor

Result:
case h.mp
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s → a✝ = s

case h.mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s

Proof state:
case h.mp
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s → a✝ = s

Tactic:
exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge

Result:
no goals

Proof state:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ∈ powersetCard (#s) s ↔ a✝ ∈ {s}

Tactic:
rw [mem_powersetCard, mem_singleton]

Result:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s ↔ a✝ = s

Proof state:
α : Type u_1
s : Finset α
⊢ powersetCard (#s) s = {s}

Tactic:
ext

Result:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ∈ powersetCard (#s) s ↔ a✝ ∈ {s}

Proof state:
case h.mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s

Tactic:
rintro rfl

Result:
case h.mpr
α : Type u_1
a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ #a✝ = #a✝