harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
theorem IsSelfAdjoint.val_re_map_spectrum {a : A} (ha : IsSelfAdjoint a) :
    spectrum ℂ a = ((↑) ∘ re '' spectrum ℂ a : Set ℂ) :=
  le_antisymm (fun z hz => ⟨z, hz, (ha.mem_spectrum_eq_re hz).symm⟩) fun z => by
    rintro ⟨z, hz, rfl⟩
    simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
⊢ z ∈ ofReal ∘ re '' σ ℂ a → z ∈ σ ℂ a

Tactic:
rintro ⟨z, hz, rfl⟩

Result:
case intro.intro
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ (ofReal ∘ re) z ∈ σ ℂ a

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ (ofReal ∘ re) z ∈ σ ℂ a

Tactic:
simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem count_attach [DecidableEq α] (l : Vector α n) (a : {x // x ∈ l}) :
    l.attach.count a = l.count ↑a

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : Array α
a : { x // x ∈ { toArray := l, size_toArray := ⋯ } }
⊢ count a { toArray := l, size_toArray := ⋯ }.attach = count a.val { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : DecidableEq α
l : Vector α n
a : { x // x ∈ l }
⊢ count a l.attach = count a.val l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : Array α
a : { x // x ∈ { toArray := l, size_toArray := ⋯ } }
⊢ count a { toArray := l, size_toArray := ⋯ }.attach = count a.val { toArray := l, size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_filter (p : α → Bool) (f : α → Option β) (l : Array α) :
    filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
toList✝ : List α
⊢ filterMap f (filter p { toList := toList✝ }) =
    filterMap (fun x => if p x = true then f x else none) { toList := toList✝ }

Tactic:
simp [List.filterMap_filter]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : Array α
⊢ filterMap f (filter p l) = filterMap (fun x => if p x = true then f x else none) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
toList✝ : List α
⊢ filterMap f (filter p { toList := toList✝ }) =
    filterMap (fun x => if p x = true then f x else none) { toList := toList✝ }
-- Mathlib/Data/Seq/Seq.lean
theorem getElem?_toList (s : Seq α) (h : s.Terminates) (n : ℕ) : (toList s h)[n]? = s.get? n

Proof state:
case a
α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
a : α
ha : s.get? m = some a
⊢ ¬s.get? m = none

Tactic:
simp [ha]

Result:
no goals

Proof state:
case a
α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
⊢ ¬s.get? m = none

Tactic:
let ⟨a, ha⟩ := ge_stable s hmn h

Result:
case a
α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
a : α
ha : s.get? m = some a
⊢ ¬s.get? m = none

Proof state:
case a
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ s.get? n = some k → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none

Tactic:
intro h m hmn

Result:
case a
α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
⊢ ¬s.get? m = none

Proof state:
case a
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ k ∈ (s.toList h)[n]? ↔ k ∈ s.get? n

Tactic:
simp only [ofList, toList, get?_mk, Option.mem_def, getElem?_take, Nat.lt_find_iff, length,
  Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt, List.get?_eq_getElem?]

Result:
case a
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ s.get? n = some k → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none

Proof state:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
⊢ (s.toList h)[n]? = s.get? n

Tactic:
ext k

Result:
case a
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ k ∈ (s.toList h)[n]? ↔ k ∈ s.get? n
-- Mathlib/Combinatorics/HalesJewett.lean
@[simp] lemma toSubspaceUnit_isMono {C : (ι → α) → κ} : l.toSubspaceUnit.IsMono C ↔ l.IsMono C

Proof state:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ (∃ c, ∀ (x : Unit → α), C (↑l (x ())) = c) ↔ ∃ c, ∀ (x : α), C (↑l x) = c

Tactic:
exact exists_congr fun c ↦ ⟨fun h a ↦ h fun _ ↦ a, fun h a ↦ h _⟩

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l

Tactic:
simp only [Subspace.IsMono, toSubspaceUnit_apply, IsMono]

Result:
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ (∃ c, ∀ (x : Unit → α), C (↑l (x ())) = c) ↔ ∃ c, ∀ (x : α), C (↑l x) = c
-- Mathlib/RingTheory/Valuation/Discrete/Basic.lean
/-- A discrete valuation on a field `K` is surjective. -/
lemma IsDiscrete.surj (v : Valuation K ℤₘ₀) [hv : IsDiscrete v] :
    Surjective v

Proof state:
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
hv : v.IsDiscrete
⊢ Surjective ⇑v

Tactic:
intro c

Result:
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
hv : v.IsDiscrete
c : ℤₘ₀
⊢ ∃ a, v a = c

Proof state:
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
hv : v.IsDiscrete
c : ℤₘ₀
⊢ ∃ a, v a = c

Tactic:
obtain ⟨π, hπ⟩ := hv

Result:
case mk.intro
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
c : ℤₘ₀
π : K
hπ : v π = ↑(ofAdd (-1))
⊢ ∃ a, v a = c

Proof state:
case mk.intro
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
c : ℤₘ₀
π : K
hπ : v π = ↑(ofAdd (-1))
a : Multiplicative ℤ
⊢ v (π ^ (-toAdd a)) = ↑a

Tactic:
simp [hπ, ← WithZero.ofAdd_zpow]

Result:
no goals

Proof state:
case mk.intro
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
c : ℤₘ₀
π : K
hπ : v π = ↑(ofAdd (-1))
⊢ ∃ a, v a = c

Tactic:
refine WithZero.cases_on c ⟨0, map_zero _⟩ fun a ↦ ⟨π ^ (-a.toAdd), ?_⟩

Result:
case mk.intro
K : Type u_2
inst✝ : Field K
v : Valuation K ℤₘ₀
c : ℤₘ₀
π : K
hπ : v π = ↑(ofAdd (-1))
a : Multiplicative ℤ
⊢ v (π ^ (-toAdd a)) = ↑a
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sigma_eq_iff_blocks_eq {c : Σn, Composition n} {c' : Σn, Composition n} :
    c = c' ↔ c.2.blocks = c'.2.blocks

Proof state:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ n = n'

Tactic:
rw [← c.blocks_sum, ← c'.blocks_sum, H]

Result:
no goals

Proof state:
c c' : (n : ℕ) × Composition n
⊢ c = c' ↔ c.snd.blocks = c'.snd.blocks

Tactic:
refine ⟨fun H => by rw [H], fun H => ?_⟩

Result:
c c' : (n : ℕ) × Composition n
H : c.snd.blocks = c'.snd.blocks
⊢ c = c'

Proof state:
case mk.mk
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
this : n = n'
⊢ ⟨n, c⟩ = ⟨n', c'⟩

Tactic:
induction this

Result:
case mk.mk.refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n, c'⟩

Proof state:
c c' : (n : ℕ) × Composition n
H : c = c'
⊢ c.snd.blocks = c'.snd.blocks

Tactic:
rw [H]

Result:
no goals

Proof state:
case mk.mk.refl.e_snd
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c = c'

Tactic:
ext1

Result:
case mk.mk.refl.e_snd.blocks
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c.blocks = c'.blocks

Proof state:
case mk
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H : ⟨n, c⟩.snd.blocks = c'.snd.blocks
⊢ ⟨n, c⟩ = c'

Tactic:
rcases c' with ⟨n', c'⟩

Result:
case mk.mk
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n', c'⟩

Proof state:
case mk.mk.refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n, c'⟩

Tactic:
congr

Result:
case mk.mk.refl.e_snd
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c = c'

Proof state:
c c' : (n : ℕ) × Composition n
H : c.snd.blocks = c'.snd.blocks
⊢ c = c'

Tactic:
rcases c with ⟨n, c⟩

Result:
case mk
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H : ⟨n, c⟩.snd.blocks = c'.snd.blocks
⊢ ⟨n, c⟩ = c'

Proof state:
case mk.mk.refl.e_snd.blocks
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c.blocks = c'.blocks

Tactic:
exact H

Result:
no goals

Proof state:
case mk.mk
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n', c'⟩

Tactic:
have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]

Result:
case mk.mk
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
this : n = n'
⊢ ⟨n, c⟩ = ⟨n', c'⟩
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem sin_eq_neg_one_iff {x : ℂ} : sin x = -1 ↔ ∃ k : ℤ, -(π / 2) + k * (2 * π) = x

Proof state:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x + ↑π / 2) ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x

Tactic:
simp only [← sub_eq_neg_add, sub_eq_iff_eq_add]

Result:
no goals

Proof state:
x : ℂ
⊢ sin x = -1 ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x

Tactic:
rw [← neg_eq_iff_eq_neg, ← cos_add_pi_div_two, cos_eq_one_iff]

Result:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x + ↑π / 2) ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x
-- Mathlib/Algebra/Ring/Rat.lean
@[simp] lemma mul_den_eq_num (q : ℚ) : q * q.den = q.num

Proof state:
q : ℚ
this : q * (↑q.den /. 1) = q.num /. 1
⊢ q * (↑q.den /. 1) = q.num /. 1

Tactic:
assumption

Result:
no goals

Proof state:
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q.num /. ↑q.den * ↑q.den = ↑q.num

Tactic:
simp only [intCast_eq_divInt, natCast_eq_divInt, num_divInt_den] at this ⊢

Result:
q : ℚ
this : q * (↑q.den /. 1) = q.num /. 1
⊢ q * (↑q.den /. 1) = q.num /. 1

Proof state:
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q * ↑q.den = ↑q.num

Tactic:
conv => pattern (occs := 1) q; (rw [← num_divInt_den q])

Result:
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q.num /. ↑q.den * ↑q.den = ↑q.num

Proof state:
q : ℚ
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1

Tactic:
have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero

Result:
q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1

Proof state:
q : ℚ
⊢ q * ↑q.den = ↑q.num

Tactic:
suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by
  conv => pattern (occs := 1) q; (rw [← num_divInt_den q])
  simp only [intCast_eq_divInt, natCast_eq_divInt, num_divInt_den] at this ⊢; assumption

Result:
q : ℚ
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1

Proof state:
q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1

Tactic:
rw [divInt_mul_divInt _ _ this Int.one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem le_gauge_of_subset_closedBall (hs : Absorbent ℝ s) (hr : 0 ≤ r) (hsr : s ⊆ closedBall 0 r) :
    ‖x‖ / r ≤ gauge s x

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ gauge (closedBall 0 r) x ≤ gauge s x

Tactic:
exact gauge_mono hs hsr _

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ ‖x‖ / r ≤ gauge s x

Tactic:
rw [← gauge_closedBall hr]

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ gauge (closedBall 0 r) x ≤ gauge s x
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_ne_zero_iff_eq_or {n : ℕ} : μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1

Proof state:
n : ℕ
⊢ μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1

Tactic:
have := moebius_eq_or n

Result:
n : ℕ
this : μ n = 0 ∨ μ n = 1 ∨ μ n = -1
⊢ μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1

Proof state:
n : ℕ
this : μ n = 0 ∨ μ n = 1 ∨ μ n = -1
⊢ μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1

Tactic:
aesop

Result:
no goals
-- Mathlib/Probability/Kernel/WithDensity.lean
nonrec lemma withDensity_congr_ae (κ : Kernel α β) [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞}
    (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g))
    (hfg : ∀ a, f a =ᵐ[κ a] g a) :
    withDensity κ f = withDensity κ g

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᶠ[ae (κ a)] g a
⊢ κ.withDensity f = κ.withDensity g

Tactic:
ext a

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᶠ[ae (κ a)] g a
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity f) a) s✝ = ((κ.withDensity g) a) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᶠ[ae (κ a)] g a
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity f) a) s✝ = ((κ.withDensity g) a) s✝

Tactic:
rw [Kernel.withDensity_apply _ hf,Kernel.withDensity_apply _ hg, withDensity_congr_ae (hfg a)]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_single_index {a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 1) :
    (single a b).prod h = h a b :=
  calc
    (single a b).prod h = ∏ x ∈ {a}, h x (single a b x) :=
      prod_of_support_subset _ support_single_subset h fun _ hx =>
        (mem_singleton.1 hx).symm ▸ h_zero
    _ = h a b

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
a : α
b : M
h : α → M → N
h_zero : h a 0 = 1
⊢ ∏ x ∈ {a}, h x ((single a b) x) = h a b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem Nonempty.sup_eq_top_iff {α : Type*} [LinearOrder α] [BoundedOrder α]
    {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Proof state:
case inr
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
exact Finset.sup_eq_top_iff

Result:
no goals

Proof state:
case inl
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Subsingleton α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simpa [Subsingleton.elim _ (⊤ : α)]

Result:
no goals

Proof state:
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
cases subsingleton_or_nontrivial α

Result:
case inl
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Subsingleton α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

case inr
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem mem_support_ofFinset_iff (a : α) : a ∈ (ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0

Proof state:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : ∑ a ∈ s, f a = 1
h' : ∀ a ∉ s, f a = 0
a : α
⊢ a ∈ (ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem Connected.dist_eq_zero_iff (hconn : G.Connected) :
    G.dist u v = 0 ↔ u = v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
hconn : G.Connected
⊢ G.dist u v = 0 ↔ u = v

Tactic:
simp [hconn u v]

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem neg_mem (h : A ∈ symplecticGroup l R) : -A ∈ symplecticGroup l R

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A * J l R * Aᵀ = J l R
⊢ -A * J l R * (-A)ᵀ = J l R

Tactic:
simp [h]

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R

Tactic:
rw [mem_iff] at h ⊢

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A * J l R * Aᵀ = J l R
⊢ -A * J l R * (-A)ᵀ = J l R
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_zero_eq_head (l : List α) (h : 0 < l.length) :
    l[0] = head l (by simpa [length_pos] using h)

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h : 0 < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝)[0] = (head✝ :: tail✝).head ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.105748
l : List α
h : 0 < l.length
⊢ l ≠ []

Tactic:
simpa [length_pos] using h

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : 0 < l.length
⊢ l[0] = l.head ⋯

Tactic:
cases l with
| nil => simp at h
| cons _ _ => simp

Result:
no goals

Proof state:
case nil
α : Type u_1
h : 0 < [].length
⊢ [][0] = [].head ⋯

Tactic:
simp at h

Result:
no goals
-- Mathlib/ModelTheory/LanguageMap.lean
theorem constantsOnMap_isExpansionOn {f : α → β} {fα : α → M} {fβ : β → M} (h : fβ ∘ f = fα) :
    @LHom.IsExpansionOn _ _ (LHom.constantsOnMap f) M (constantsOn.structure fα)
      (constantsOn.structure fβ)

Proof state:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this : (constantsOn α).Structure M := constantsOn.structure fα
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
letI := constantsOn.structure fβ

Result:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this✝ : (constantsOn α).Structure M := constantsOn.structure fα
this : (constantsOn β).Structure M := constantsOn.structure fβ
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Proof state:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this✝ : (constantsOn α).Structure M := constantsOn.structure fα
this : (constantsOn β).Structure M := constantsOn.structure fβ
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
exact
  ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F :)) fun n F => isEmptyElim F, fun R =>
    isEmptyElim R⟩

Result:
no goals

Proof state:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
letI := constantsOn.structure fα

Result:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this : (constantsOn α).Structure M := constantsOn.structure fα
⊢ (LHom.constantsOnMap f).IsExpansionOn M
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem Measure.isTopologicalBasis_isOpen_lt_top [TopologicalSpace α]
    (μ : Measure α) [IsLocallyFiniteMeasure μ] :
    TopologicalSpace.IsTopologicalBasis { s | IsOpen s ∧ μ s < ∞ }

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
⊢ ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, x ∈ v ∧ v ⊆ s

Tactic:
rcases μ.exists_isOpen_measure_lt_top x with ⟨v, xv, hv, μv⟩

Result:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : μ v < ⊤
⊢ ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, x ∈ v ∧ v ⊆ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ⊤}

Tactic:
refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds (fun s hs => hs.1) ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, a ∈ v ∧ v ⊆ u

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, a ∈ v ∧ v ⊆ u

Tactic:
intro x s xs hs

Result:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
⊢ ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, x ∈ v ∧ v ⊆ s

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : μ v < ⊤
⊢ ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, x ∈ v ∧ v ⊆ s

Tactic:
refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩

Result:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : μ v < ⊤
⊢ μ (v ∩ s) ≤ μ v

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : μ v < ⊤
⊢ μ (v ∩ s) ≤ μ v

Tactic:
exact measure_mono inter_subset_left

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerLeft_comp {f g h i : C}
    {η : h ⟶ i} {η₁ : g ⊗ h ⟶ g ⊗ i} {η₂ : f ⊗ g ⊗ h ⟶ f ⊗ g ⊗ i}
    {η₃ : f ⊗ g ⊗ h ⟶ (f ⊗ g) ⊗ i} {η₄ : (f ⊗ g) ⊗ h ⟶ (f ⊗ g) ⊗ i}
    (e_η₁ : g ◁ η = η₁) (e_η₂ : f ◁ η₁ = η₂)
    (e_η₃ : η₂ ≫ (α_ _ _ _).inv = η₃) (e_η₄ : (α_ _ _ _).hom ≫ η₃ = η₄) :
    (f ⊗ g) ◁ η = η₄

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : h ⟶ i
η₁ : g ⊗ h ⟶ g ⊗ i
η₂ : f ⊗ g ⊗ h ⟶ f ⊗ g ⊗ i
η₃ : f ⊗ g ⊗ h ⟶ (f ⊗ g) ⊗ i
η₄ : (f ⊗ g) ⊗ h ⟶ (f ⊗ g) ⊗ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ⊗ g) ◁ η = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem affineSpan_pair_parallel_iff_vectorSpan_eq {p₁ p₂ p₃ p₄ : P} :
    line[k, p₁, p₂] ∥ line[k, p₃, p₄] ↔
      vectorSpan k ({p₁, p₂} : Set P) = vectorSpan k ({p₃, p₄} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
⊢ affineSpan k {p₁, p₂} ∥ affineSpan k {p₃, p₄} ↔ vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}

Tactic:
simp [affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, ←
  not_nonempty_iff_eq_empty]

Result:
no goals