harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`. -/
lemma binEntropy_neg_of_neg (hp : p < 0) : binEntropy p < 0

Proof state:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
this : log p < log (1 - p)
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
nlinarith [log_pos_of_lt_neg_one hp']

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log (-p) < log (1 - p)

Tactic:
exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p < 1 - p

Tactic:
linarith

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ 1 < 1 - p

Tactic:
linarith

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p ≤ 0

Tactic:
wlog h : -1 < p

Result:
case inr
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0

p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0

Proof state:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
have : log p < log (1 - p) := by
  rw [← log_neg_eq_log]
  exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)

Result:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
this : log p < log (1 - p)
⊢ -p * log p < (1 - p) * log (1 - p)

Proof state:
case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
nlinarith [(log_pos (by linarith) : 0 < log (1 - p))]

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
this : -p * log p < (1 - p) * log (1 - p)
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Tactic:
linarith

Result:
no goals

Proof state:
case inr
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0

Tactic:
simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]

Result:
no goals

Proof state:
p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0

Tactic:
nlinarith [log_neg_of_lt_zero hp h]

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log p < log (1 - p)

Tactic:
rw [← log_neg_eq_log]

Result:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log (-p) < log (1 - p)

Proof state:
p : ℝ
hp : p < 0
⊢ binEntropy p < 0

Tactic:
rw [binEntropy, log_inv, log_inv]

Result:
p : ℝ
hp : p < 0
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Proof state:
p : ℝ
hp : p < 0
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
by_cases hp' : p < -1

Result:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Proof state:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ p = -1

Tactic:
linarith

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Tactic:
suffices -p * log p < (1 - p) * log (1 - p) by linarith

Result:
p : ℝ
hp : p < 0
⊢ -p * log p < (1 - p) * log (1 - p)
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_lt_iff_left (hb : AddLECancellable b) (hba : b ≤ a) :
    a - b < c ↔ a < b + c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c

Tactic:
refine (tsub_le_iff_left.mpr h.le).lt_of_ne ?_

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b ≠ c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a < b + c → a - b < c

Tactic:
intro h

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
refine ⟨hb.lt_add_of_tsub_lt_left, ?_⟩

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a < b + c → a - b < c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False

Tactic:
exact h.ne' (add_tsub_cancel_of_le hba)

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b ≠ c

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem contDiffOn_stereoToFun {n : WithTop ℕ∞} :
    ContDiffOn ℝ n (stereoToFun v) {x : E | innerSL _ v x ≠ (1 : ℝ)}

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n (fun x => 2 / (1 - ((innerSL ℝ) v) x)) {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
refine contDiff_const.contDiffOn.div ?_ ?_

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n (fun x => 1 - ((innerSL ℝ) v) x) {x | ((innerSL ℝ) v) x ≠ 1}

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ∀ x ∈ {x | ((innerSL ℝ) v) x ≠ 1}, 1 - ((innerSL ℝ) v) x ≠ 0

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
x : E
h : x ∈ {x | ((innerSL ℝ) v) x ≠ 1}
h' : 1 - ((innerSL ℝ) v) x = 0
⊢ False

Tactic:
exact h (sub_eq_zero.mp h').symm

Result:
no goals

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n (fun x => 1 - ((innerSL ℝ) v) x) {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
exact (contDiff_const.sub (innerSL ℝ v).contDiff).contDiffOn

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
refine ContDiffOn.smul ?_ (orthogonalProjection (ℝ ∙ v)ᗮ).contDiff.contDiffOn

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n (fun x => 2 / (1 - ((innerSL ℝ) v) x)) {x | ((innerSL ℝ) v) x ≠ 1}

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
⊢ ∀ x ∈ {x | ((innerSL ℝ) v) x ≠ 1}, 1 - ((innerSL ℝ) v) x ≠ 0

Tactic:
intro x h h'

Result:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : WithTop ℕ∞
x : E
h : x ∈ {x | ((innerSL ℝ) v) x ≠ 1}
h' : 1 - ((innerSL ℝ) v) x = 0
⊢ False
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem restrict_univ (m : OuterMeasure α) : restrict univ m = m :=
  ext fun s => by simp

Proof state:
α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict univ) m) s = m s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem preimage_compl [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] {f : α → β}
    (s : Finset β) (hf : Function.Injective f) :
    preimage sᶜ f hf.injOn = (preimage s f hf.injOn)ᶜ :=
  Finset.coe_injective (by simp)

Proof state:
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
s : Finset β
hf : Injective f
⊢ ↑(sᶜ.preimage f ⋯) = ↑(s.preimage f ⋯)ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_prod_left_eq_zip {l : Vector α n} (f : α → β) :
    (l.map fun x => (x, f x)) = l.zip (l.map f)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β
⊢ map (fun x => (x, f x)) l = l.zip (map f l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => (x, f x)) { toArray := l, size_toArray := ⋯ } =
    { toArray := l, size_toArray := ⋯ }.zip (map f { toArray := l, size_toArray := ⋯ })

Proof state:
case mk.e_v
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => x) { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => (x, f x)) { toArray := l, size_toArray := ⋯ } =
    { toArray := l, size_toArray := ⋯ }.zip (map f { toArray := l, size_toArray := ⋯ })

Tactic:
rw [← zip_map']

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ (map (fun x => x) { toArray := l, size_toArray := ⋯ }).zip (map f { toArray := l, size_toArray := ⋯ }) =
    { toArray := l, size_toArray := ⋯ }.zip (map f { toArray := l, size_toArray := ⋯ })

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ (map (fun x => x) { toArray := l, size_toArray := ⋯ }).zip (map f { toArray := l, size_toArray := ⋯ }) =
    { toArray := l, size_toArray := ⋯ }.zip (map f { toArray := l, size_toArray := ⋯ })

Tactic:
congr

Result:
case mk.e_v
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => x) { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem pi_eq_zero : pi fv = 0 ↔ ∀ i, fv i = 0

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
fv : (i : ι) → P1 →ᵃ[k] φv i
⊢ pi fv = 0 ↔ ∀ (i : ι), fv i = 0

Tactic:
simp only [AffineMap.ext_iff, funext_iff, pi_apply]

Result:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
fv : (i : ι) → P1 →ᵃ[k] φv i
⊢ (∀ (p : P1) (x : ι), (fv x) p = 0 p x) ↔ ∀ (i : ι) (p : P1), (fv i) p = 0 p

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
fv : (i : ι) → P1 →ᵃ[k] φv i
⊢ (∀ (p : P1) (x : ι), (fv x) p = 0 p x) ↔ ∀ (i : ι) (p : P1), (fv i) p = 0 p

Tactic:
exact forall_comm

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem ext_ring {f g : R →ₑ+[σ] N'} (h : f 1 = g 1) : f = g

Proof state:
R : Type u_11
inst✝³ : Semiring R
S : Type u_12
inst✝² : Semiring S
N' : Type u_14
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
⊢ f = g

Tactic:
ext x

Result:
case a
R : Type u_11
inst✝³ : Semiring R
S : Type u_12
inst✝² : Semiring S
N' : Type u_14
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ f x = g x

Proof state:
case a
R : Type u_11
inst✝³ : Semiring R
S : Type u_12
inst✝² : Semiring S
N' : Type u_14
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_mul_eq_inter' (hms : MeasurableSet s) (hcs' : μ s ≠ ∞) (t : Set Ω) :
    μ[t|s] * μ s = μ (s ∩ t)

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ⊤
t : Set Ω
hcs : μ s = 0
⊢ μ[t | s] * μ s = μ (s ∩ t)

Tactic:
simp [hcs, measure_inter_null_of_null_left]

Result:
no goals

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ⊤
t : Set Ω
hcs : μ s ≠ 0
⊢ μ[t | s] * μ s = μ (s ∩ t)

Tactic:
rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ⊤
t : Set Ω
⊢ μ[t | s] * μ s = μ (s ∩ t)

Tactic:
obtain hcs | hcs := eq_or_ne (μ s) 0

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ⊤
t : Set Ω
hcs : μ s = 0
⊢ μ[t | s] * μ s = μ (s ∩ t)

case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ⊤
t : Set Ω
hcs : μ s ≠ 0
⊢ μ[t | s] * μ s = μ (s ∩ t)
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_iInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    {ι : Sort x} (f : ι → α) (hf : ∀ i, u (l (f i)) = f i) : l (⨅ i, f i) = ⨅ i, l (f i) :=
  calc
    l (⨅ i, f i) = l (⨅ i : ι, u (l (f i)))

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
f : ι → α
hf : ∀ (i : ι), u (l (f i)) = f i
⊢ l (⨅ i, f i) = l (⨅ i, u (l (f i)))

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_append (p : G.Walk u v) (q : G.Walk v w) :
    (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

Tactic:
induction p <;> simp [*, sup_assoc]

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_zero_right [HasImages V] {w} :
    imageToKernel f (0 : B ⟶ C) w =
      (imageSubobject f).arrow ≫ inv (kernelSubobject (0 : B ⟶ C)).arrow

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w = (imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow

Tactic:
ext

Result:
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w ≫ (kernelSubobject 0).arrow =
    ((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow) ≫ (kernelSubobject 0).arrow

Proof state:
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w ≫ (kernelSubobject 0).arrow =
    ((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow) ≫ (kernelSubobject 0).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_filterMap_of_eq_some {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.head w) = some b) :
    (filterMap f l).head ((ne_nil_of_mem (mem_filterMap.2 ⟨_, head_mem w, h⟩))) =
      b

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
a : α
l : List α
w : a :: l ≠ []
h : f ((a :: l).head w) = some b
⊢ (filterMap f (a :: l)).head ⋯ = b

Tactic:
simp only [head_cons] at h

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
a : α
l : List α
w : a :: l ≠ []
h : f a = some b
⊢ (filterMap f (a :: l)).head ⋯ = b

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
b : β
w : [] ≠ []
h : f ([].head w) = some b
⊢ (filterMap f []).head ⋯ = b

Tactic:
simp at w

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
a : α
l : List α
w : a :: l ≠ []
h : f a = some b
⊢ (filterMap f (a :: l)).head ⋯ = b

Tactic:
simp [filterMap_cons, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
w : l ≠ []
b : β
h : f (l.head w) = some b
⊢ (filterMap f l).head ⋯ = b

Tactic:
cases l with
| nil => simp at w
| cons a l =>
  simp only [head_cons] at h
  simp [filterMap_cons, h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_left_injective {x : ℝ} (hx : x ≠ 0) : Function.Injective fun y : ℝ≥0 => y ^ x :=
  fun y z hyz => by simpa only [rpow_inv_rpow_self hx] using congr_arg (fun y => y ^ (1 / x)) hyz

Proof state:
x : ℝ
hx : x ≠ 0
y z : ℝ≥0
hyz : (fun y => y ^ x) y = (fun y => y ^ x) z
⊢ y = z

Tactic:
simpa only [rpow_inv_rpow_self hx] using congr_arg (fun y => y ^ (1 / x)) hyz

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem ofMultiset_apply_of_not_mem {a : α} (ha : a ∉ s) : ofMultiset s hs a = 0

Proof state:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s
⊢ (ofMultiset s hs) a = 0

Tactic:
simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero,
  ENNReal.natCast_ne_top, or_false] using ha

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_pos_iff {x : R} : 0 < star x ↔ 0 < x

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 0 < star x ↔ 0 < x

Tactic:
simpa using star_lt_star_iff (x := 0) (y := x)

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem strictMono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictMono f

Tactic:
rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/MonoCoprod.lean
lemma mono_inj (c : Cofan X) (h : IsColimit c) (i : I)
    [HasCoproduct (fun (k : ((Set.range (fun _ : Unit ↦ i))ᶜ : Set I)) => X k.1)] :
    Mono (Cofan.inj c i)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k => X ↑k
ι : Unit → I := fun x => i
⊢ Mono (c.inj i)

Tactic:
have hι : Function.Injective ι := fun _ _ _ ↦ rfl

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k => X ↑k
ι : Unit → I := fun x => i
hι : Function.Injective ι
⊢ Mono (c.inj i)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k => X ↑k
ι : Unit → I := fun x => i
hι : Function.Injective ι
⊢ Mono (c.inj i)

Tactic:
exact mono_of_injective X ι hι c (Cofan.mk (X i) (fun _ ↦ 𝟙 _)) h
  (mkCofanColimit _ (fun s => s.inj ()))

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k => X ↑k
⊢ Mono (c.inj i)

Tactic:
let ι : Unit → I := fun _ ↦ i

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k => X ↑k
ι : Unit → I := fun x => i
⊢ Mono (c.inj i)
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem someExistsOneDivLT_subset : someExistsOneDivLT s i ⊆ i

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i

Tactic:
by_cases hi : ¬s ≤[i] 0

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ ∅ ⊆ i

Tactic:
exact Set.empty_subset _

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i

Tactic:
exact
  let ⟨h, _⟩ := someExistsOneDivLT_spec hi
  h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i

Tactic:
rw [someExistsOneDivLT, dif_neg hi]

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ ∅ ⊆ i
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_mul_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) :
    ↑(q * r) = (q * r : α)

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.num * ↑r.num / (↑q.den * ↑r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

Tactic:
rfl

Result:
no goals

Proof state:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
push_cast

Result:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.num) / ↑(q.den * r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

Tactic:
push_cast

Result:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.num * ↑r.num / (↑q.den * ↑r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q * r) = ↑q * ↑r

Tactic:
rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
  (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Result:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.num) / ↑(q.den * r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Proof state:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Tactic:
exact mul_ne_zero hq hr

Result:
no goals