harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem exists_dist_lt_le (hδ : 0 < δ) (hε : 0 ≤ ε) (h : dist x z < ε + δ) :
    ∃ y, dist x y < δ ∧ dist y z ≤ ε

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
y : E
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ ∃ y, dist x y < δ ∧ dist y z ≤ ε

Tactic:
exact ⟨y, by simp [dist_comm x y, dist_comm y z, *]⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z ≤ ε

Tactic:
obtain ⟨y, yz, xy⟩ :=
  exists_dist_le_lt hε hδ (show dist z x < δ + ε by simpa only [dist_comm, add_comm] using h)

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
y : E
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ ∃ y, dist x y < δ ∧ dist y z ≤ ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
y : E
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ dist x y < δ ∧ dist y z ≤ ε

Tactic:
simp [dist_comm x y, dist_comm y z, *]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
⊢ dist z x < δ + ε

Tactic:
simpa only [dist_comm, add_comm] using h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem tsum_indicator_apply_singleton [Countable α] [MeasurableSingletonClass α] (μ : Measure α)
    (s : Set α) (hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ {x}) x) = μ s

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (fun x => μ {x}) x = μ s

Tactic:
classical
calc
  (∑' x : α, s.indicator (fun x => μ {x}) x) =
    Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
    simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
      Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]
  _ = μ s := by rw [μ.sum_smul_dirac]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (fun x => μ {x}) x = (sum fun a => μ {a} • dirac a) s

Tactic:
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
  Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (fun x => μ {x}) x = μ s

Tactic:
calc
  (∑' x : α, s.indicator (fun x => μ {x}) x) =
    Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
    simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
      Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]
  _ = μ s := by rw [μ.sum_smul_dirac]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum fun a => μ {a} • dirac a) s = μ s

Tactic:
rw [μ.sum_smul_dirac]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a

Proof state:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ (n - ↑b + ↑a) % n = ↑a - ↑b ↔ ↑b ≤ ↑a

Tactic:
rw [Nat.mod_eq_sub_of_lt_two_mul h]

Result:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a - n = ↑a - ↑b ↔ ↑b ≤ ↑a

n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < 2 * n

Proof state:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ (n - ↑b + ↑a) % n = ↑a - ↑b ↔ ↑b ≤ ↑a

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a = ↑a - ↑b ↔ ↑b ≤ ↑a

n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < n

Proof state:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < 2 * n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
⊢ (n - ↑b + ↑a) % n = ↑a - ↑b ↔ ↑b ≤ ↑a

Tactic:
if h : n ≤ (n - b) + a then
  rw [Nat.mod_eq_sub_of_lt_two_mul h]
  all_goals omega
else
  rw [Nat.mod_eq_of_lt]
  all_goals omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a - n = ↑a - ↑b ↔ ↑b ≤ ↑a

n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < 2 * n

Tactic:
all_goals omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a

Tactic:
rw [sub_def, le_def]

Result:
n : Nat
a b : Fin n
⊢ ↑⟨(n - ↑b + ↑a) % n, ⋯⟩ = ↑a - ↑b ↔ ↑b ≤ ↑a

Proof state:
n : Nat
a b : Fin n
⊢ ↑⟨(n - ↑b + ↑a) % n, ⋯⟩ = ↑a - ↑b ↔ ↑b ≤ ↑a

Tactic:
dsimp only

Result:
n : Nat
a b : Fin n
⊢ (n - ↑b + ↑a) % n = ↑a - ↑b ↔ ↑b ≤ ↑a

Proof state:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a = ↑a - ↑b ↔ ↑b ≤ ↑a

n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < n

Tactic:
all_goals omega

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem Ici_iSup₂ (f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⋂ (i) (j), Ici (f i j)

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Ici (f i j)

Tactic:
simp_rw [Ici_iSup]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_eq_top_iff : infEdist x s = ∞ ↔ s = ∅

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infEdist x s = ⊤ ↔ s = ∅

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [*, Nonempty.ne_empty, infEdist_ne_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
    getKey k' (alterKey k f l) hc =
      if heq : k == k' then
        k
      else
        haveI h' : containsKey k' l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l
⊢ getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l ⋯

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l
h✝ : (k == k') = true
⊢ getKey k' (alterKey k f l) hc = k

case isFalse
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l
h✝ : ¬(k == k') = true
⊢ getKey k' (alterKey k f l) hc = getKey k' l ⋯

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l
heq : ¬(k == k') = true
⊢ some (getKey k' (alterKey k f l) hc) = some (getKey k' l ⋯)

Tactic:
simp_all only [Bool.false_eq_true, ite_false]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
heq : ¬(k == k') = true
this : some (getKey k' (alterKey k f l) hc) = getKey? k' l
⊢ getKey? k' l = some (getKey k' l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
heq : ¬(k == k') = true
this : some (getKey k' (alterKey k f l) hc) = getKey? k' l
⊢ getKey? k' l = some (getKey k' l ⋯)

Tactic:
rw [getKey?_eq_some_getKey]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_eq_arcsin_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) : ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, angle_add_eq_arcsin_of_inner_eq_zero h h0]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_rpow_of_exponent_lt (hx : 1 < x) (hyz : y < z) : x ^ y < x ^ z

Proof state:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)

Tactic:
rw [exp_lt_exp]

Result:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z

Proof state:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Result:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)

Proof state:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z

Tactic:
exact mul_lt_mul_of_pos_left hyz (log_pos hx)

Result:
no goals

Proof state:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < x ^ z

Tactic:
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Result:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_zpow (f : R → R) (n : ℤ) (a : Aˣ)
    (hf : ContinuousOn f ((· ^ n) '' (spectrum R (a : A)))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : HasContinuousInv₀ R
inst✝ : UniqueHom R A
f : R → R
n : ℤ
a : Aˣ
hf : autoParam (ContinuousOn f ((fun x => x ^ n) '' spectrum R ↑a)) _auto✝
ha : autoParam (p ↑a) _auto✝
⊢ cfc (fun x => f (x ^ n)) ↑a = cfc f ↑(a ^ n)

Tactic:
rw [cfc_comp' .., cfc_zpow a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a

Proof state:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
xs : List α
h₁ : a ∈ xs
h₂ : ∀ (b : α), b ∈ xs → b ≤ a
⊢ xs.max? = some a

Tactic:
cases xs with
| nil => simp at h₁
| cons x xs =>
  exact congrArg some <| anti.1 _ _
    (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
    ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
xs : List α
⊢ (a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a) → xs.max? = some a

Tactic:
intro ⟨h₁, h₂⟩

Result:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
xs : List α
h₁ : a ∈ xs
h₂ : ∀ (b : α), b ∈ xs → b ≤ a
⊢ xs.max? = some a

Proof state:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
xs : List α
⊢ xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a

Tactic:
refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩

Result:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
xs : List α
⊢ (a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a) → xs.max? = some a

Proof state:
case nil
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
h₁ : a ∈ []
h₂ : ∀ (b : α), b ∈ [] → b ≤ a
⊢ [].max? = some a

Tactic:
simp at h₁

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
x : α
xs : List α
h₁ : a ∈ x :: xs
h₂ : ∀ (b : α), b ∈ x :: xs → b ≤ a
⊢ (x :: xs).max? = some a

Tactic:
exact congrArg some <| anti.1 _ _
  (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
  ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_eq_cons_iff {xs : List α} {a : α} {ys : List α} :
    xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]

Proof state:
α : Type u_1
xs : List α
a : α
ys : List α
⊢ xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]

Tactic:
rw [reverse_eq_iff, reverse_cons]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma one_top : IsConjExponent 1 ∞ := ⟨by simp⟩

Proof state:
⊢ 1⁻¹ + ⊤⁻¹ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem setOf_isPreconnected_subset_of_ordered :
    { s : Set α | IsPreconnected s } ⊆
      -- bounded intervals
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo)) ∪
      -- unbounded intervals and `univ`
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ {s | IsPreconnected s} ⊆
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
intro s hs

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : s ∈ {s | IsPreconnected s}
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : s ∈ {s | IsPreconnected s}
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs) <;> rw [hs] <;>
  simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
    uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Even.const_smul [SMul β γ] (hg : g.Even) (r : β) : (r • g).Even

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
⊢ Function.Even (r • g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
a : α
⊢ (r • g) (-a) = (r • g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
a : α
⊢ (r • g) (-a) = (r • g) a

Tactic:
simp only [Pi.smul_apply, hg a]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[nontriviality]
lemma apply_eq_zero_of_isEmpty [IsEmpty α] {_ : MeasurableSpace α} (μ : Measure α) (s : Set α) :
    μ s = 0

Proof state:
α : Type u_1
inst✝ : IsEmpty α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = 0

Tactic:
rw [eq_empty_of_isEmpty s, measure_empty]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_eq_sin_div_cos : tan x = sin x / cos x :=
  ofReal_injective <| by simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
    ofReal_cos]

Proof state:
x : ℝ
⊢ ↑(tan x) = ↑(sin x / cos x)

Tactic:
simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
ofReal_cos]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem of_union {A B : Set α} (h : Disjoint A B) (hA : MeasurableSet A) (hB : MeasurableSet B) :
    v (A ∪ B) = v A + v B

Proof state:
case hm
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

case hd
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (Disjoint on fun b => bif b then A else B)

Tactic:
exacts [fun b => Bool.casesOn b hB hA, pairwise_disjoint_on_bool.2 h]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ↑v (A ∪ B) = ↑v A + ↑v B

Tactic:
rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]

Result:
case hm
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

case hd
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (Disjoint on fun b => bif b then A else B)
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem Connected.dist_triangle (hconn : G.Connected) :
    G.dist u w ≤ G.dist u v + G.dist v w

Proof state:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
obtain ⟨p, hp⟩ := hconn.exists_walk_length_eq_dist u v

Result:
case intro
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
rw [← hp, ← hq, ← Walk.length_append]

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ (p.append q).length

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ (p.append q).length

Tactic:
apply dist_le

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem intCast_mod (a : ℤ) (b : ℕ) : ((a % b : ℤ) : ZMod b) = (a : ZMod b)

Proof state:
a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]

Tactic:
apply Int.mod_modEq

Result:
no goals

Proof state:
a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a

Tactic:
rw [ZMod.intCast_eq_intCast_iff]

Result:
a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]