harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Connected/PathConnected.lean
theorem Topology.IsInducing.isPathConnected_iff {f : X → Y} (hf : IsInducing f) :
    IsPathConnected F ↔ IsPathConnected (f '' F)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ x ∈ F, ∀ {y : X}, y ∈ F → JoinedIn F x y) ↔ ∃ x ∈ F, ∀ ⦃x_1 : X⦄, x_1 ∈ F → JoinedIn (f '' F) (f x) (f x_1)

Tactic:
refine exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
x : X
hx : x ∈ F
y : X
hy : y ∈ F
⊢ JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
x : X
hx : x ∈ F
y : X
hy : y ∈ F
⊢ JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)

Tactic:
rw [hf.joinedIn_image hx hy]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ IsPathConnected F ↔ IsPathConnected (f '' F)

Tactic:
simp only [IsPathConnected, forall_mem_image, exists_mem_image]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ x ∈ F, ∀ {y : X}, y ∈ F → JoinedIn F x y) ↔ ∃ x ∈ F, ∀ ⦃x_1 : X⦄, x_1 ∈ F → JoinedIn (f '' F) (f x) (f x_1)
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_zero : s.bind (fun _ => 0 : α → Multiset β) = 0

Proof state:
α : Type u_1
β : Type v
s : Multiset α
⊢ (s.bind fun x => 0) = 0

Tactic:
simp [bind, join, nsmul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_toList (p : α → Bool) (v : Vector α n) :
    v.toList.any p = v.any p

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ v.toList.any p = v.any p

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.any p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.any p

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.any p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.any p

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_four : bernoulli' 4 = -1 / 30

Proof state:
⊢ bernoulli' 4 = -1 / 30

Tactic:
have : Nat.choose 4 2 = 6 := by decide

Result:
this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30

Proof state:
⊢ Nat.choose 4 2 = 6

Tactic:
decide

Result:
no goals

Proof state:
this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30

Tactic:
rw [bernoulli'_def]

Result:
this : Nat.choose 4 2 = 6
⊢ 1 - ∑ k ∈ range 4, ↑(Nat.choose 4 k) / (↑4 - ↑k + 1) * bernoulli' k = -1 / 30

Proof state:
this : Nat.choose 4 2 = 6
⊢ 1 - ∑ k ∈ range 4, ↑(Nat.choose 4 k) / (↑4 - ↑k + 1) * bernoulli' k = -1 / 30

Tactic:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero, this]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem fold_cons_key {l : Raw α β} {acc : List α} :
    l.fold (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets).reverse ++ acc

Proof state:
α : Type u
β : α → Type v
l : Raw α β
acc : List α
⊢ Raw.fold (fun acc k x => k :: acc) acc l = List.keys (toListModel l.buckets).reverse ++ acc

Tactic:
rw [fold_cons_apply, keys_eq_map, map_reverse]

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem coe_biInf : (↑(⨅ i, ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ i, ⨅ (_ : p i), (f i : α)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : IsEmpty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

case inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : Nonempty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Proof state:
case inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : Nonempty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]

Result:
no goals

Proof state:
case inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : IsEmpty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_conj : cos (conj x) = conj (cos x)

Proof state:
x : ℂ
⊢ cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cos x)

Tactic:
rw [← cosh_mul_I, ← conj_neg_I, ← RingHom.map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
lemma integral_exp_pos {μ : Measure α} {f : α → ℝ} [hμ : NeZero μ]
    (hf : Integrable (fun x ↦ Real.exp (f x)) μ) :
    0 < ∫ x, Real.exp (f x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
⊢ 0 < μ (Function.support fun x => Real.exp (f x))

Tactic:
suffices (Function.support fun x ↦ Real.exp (f x)) = Set.univ by simp [this, hμ.out]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
⊢ (Function.support fun x => Real.exp (f x)) = univ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
⊢ 0 < ∫ (x : α), Real.exp (f x) ∂μ

Tactic:
rw [integral_pos_iff_support_of_nonneg (fun x ↦ (Real.exp_pos _).le) hf]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
⊢ 0 < μ (Function.support fun x => Real.exp (f x))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
⊢ (Function.support fun x => Real.exp (f x)) = univ

Tactic:
ext1 x

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
x : α
⊢ (x ∈ Function.support fun x => Real.exp (f x)) ↔ x ∈ univ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
x : α
⊢ (x ∈ Function.support fun x => Real.exp (f x)) ↔ x ∈ univ

Tactic:
simp only [Function.mem_support, ne_eq, (Real.exp_pos _).ne', not_false_eq_true, Set.mem_univ]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x => Real.exp (f x)) μ
this : (Function.support fun x => Real.exp (f x)) = univ
⊢ 0 < μ (Function.support fun x => Real.exp (f x))

Tactic:
simp [this, hμ.out]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem reverse_isTrail_iff {u v : V} (p : G.Walk u v) : p.reverse.IsTrail ↔ p.IsTrail

Proof state:
case h.e'_5
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
⊢ p = p.reverse.reverse

Tactic:
rw [reverse_reverse]

Result:
no goals

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
convert h.reverse _

Result:
no goals

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsTrail → p.reverse.IsTrail

Tactic:
intro h

Result:
case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Proof state:
case h.e'_5
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsTrail
⊢ p = p.reverse.reverse

Tactic:
try rw [reverse_reverse]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
@[simp]
lemma egauge_univ [(𝓝[≠] (0 : 𝕜)).NeBot] : egauge 𝕜 univ x = 0

Proof state:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
⊢ egauge 𝕜 univ x = 0

Tactic:
rw [egauge_eq_zero_iff]

Result:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • univ

Proof state:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • univ

Tactic:
refine (frequently_iff_neBot.2 ‹_›).mono fun c hc ↦ ?_

Result:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ c • univ

Proof state:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ c • univ

Tactic:
simp_all [smul_set_univ₀]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq : p ≠ q) :
    (q : ZMod p) ≠ 0

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ ↑q ≠ 0

Tactic:
rwa [← Nat.cast_zero, Ne, eq_iff_modEq_nat, Nat.modEq_zero_iff_dvd, ←
  hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_zero (n : Nat) : rev 0 = last n

Proof state:
n : Nat
⊢ rev 0 = last n

Tactic:
rw [← rev_rev (last _), rev_last]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive (attr := simp)]
lemma ncard_inv (s : Set G) : s⁻¹.ncard = s.ncard

Proof state:
G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ s⁻¹.ncard = s.ncard

Tactic:
simp [ncard]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
@[simp]
lemma rTensorAlgEquiv_apply (x : (MvPolynomial σ S) ⊗[R] N) :
    rTensorAlgEquiv x = rTensorAlgHom x

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ ↑rTensorAlgEquiv x = rTensorAlgHom x

Tactic:
congr 1

Result:
case e_a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ ↑rTensorAlgEquiv = rTensorAlgHom

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ rTensorAlgEquiv x = rTensorAlgHom x

Tactic:
rw [← AlgHom.coe_coe, ← AlgEquiv.toAlgHom_eq_coe]

Result:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ ↑rTensorAlgEquiv x = rTensorAlgHom x

Proof state:
case e_a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ ↑rTensorAlgEquiv = rTensorAlgHom

Tactic:
ext _ d <;> simpa [rTensorAlgEquiv] using rTensor_apply_tmul_apply _ _ d

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem min'_singleton (a : α) : ({a} : Finset α).min' (singleton_nonempty _) = a

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min' ⋯ = a

Tactic:
simp [min']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_eq_none' {o : Option α} {f : α → Option β} :
    o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → Option β
⊢ o.bind f = none ↔ ∀ (b : β) (a : α), a ∈ o → ¬b ∈ f a

Tactic:
simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma _root_.ContDiffWithinAt.lieBracketWithin_vectorField
    {m n : WithTop ℕ∞} (hV : ContDiffWithinAt 𝕜 n V s x)
    (hW : ContDiffWithinAt 𝕜 n W s x) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx : x ∈ s) :
    ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x

Proof state:
case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 V s x) (W x)) s x

Tactic:
exact ContDiffWithinAt.clm_apply (hV.fderivWithin_right hs hmn hx)
  (hW.of_le (le_trans le_self_add hmn))

Result:
no goals

Proof state:
case hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 W s x) (V x)) s x

Tactic:
exact ContDiffWithinAt.clm_apply (hW.fderivWithin_right hs hmn hx)
  (hV.of_le (le_trans le_self_add hmn))

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x

Tactic:
apply ContDiffWithinAt.sub

Result:
case hf
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 W s x) (V x)) s x

case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 V s x) (W x)) s x
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem corecF_eq {α : Type _} (g : α → F α) (x : α) :
    PFunctor.M.dest (corecF g x) = q.P.map (corecF g) (repr (g x))

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (corecF g x).dest = (P F).map (corecF g) (repr (g x))

Tactic:
rw [corecF, PFunctor.M.dest_corec]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem flatMap_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → List β} {g : α → List β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.flatMap f) = l.unattach.flatMap g

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → List β
g : α → List β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : flatMap f l = flatMap g (map (fun x => x.val) l)
⊢ flatMap f (a :: l) = flatMap g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → List β
g : α → List β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMap f [] = flatMap g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → List β
g : α → List β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMap f l = flatMap g l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → List β
g : α → List β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMap f l = flatMap g (map (fun x => x.val) l)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → List β
g : α → List β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMap f l = flatMap g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem inter_ae_eq_empty_of_ae_eq_empty_right (h : t =ᵐ[μ] (∅ : Set α)) :
    (s ∩ t : Set α) =ᵐ[μ] (∅ : Set α)

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ ∅ = s ∩ ∅

Tactic:
rw [inter_empty]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ s ∩ t =ᶠ[ae μ] ∅

Tactic:
convert ae_eq_set_inter (ae_eq_refl s) h

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] ∅
⊢ ∅ = s ∩ ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_append_mkArray : mkArray n a ++ mkArray m a = mkArray (n + m) a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ mkArray n a ++ mkArray m a = mkArray (n + m) a

Tactic:
apply Array.ext'

Result:
case h
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (mkArray n a ++ mkArray m a).toList = (mkArray (n + m) a).toList

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (mkArray n a ++ mkArray m a).toList = (mkArray (n + m) a).toList

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_disjoint_Ico {a b c d : α} (h : b ≤ c) : Disjoint (Ico a b) (Ico c d) :=
  disjoint_left.mpr fun hab hbc => by
    rw [mem_Ico] at hab hbc
    exact hab.2.not_le (h.trans hbc.1)

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a✝ ∈ Ico a b
hbc : a✝ ∈ Ico c d
⊢ False

Tactic:
rw [mem_Ico] at hab hbc

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a ≤ a✝ ∧ a✝ < b
hbc : c ≤ a✝ ∧ a✝ < d
⊢ False

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a ≤ a✝ ∧ a✝ < b
hbc : c ≤ a✝ ∧ a✝ < d
⊢ False

Tactic:
exact hab.2.not_le (h.trans hbc.1)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_map : (p.map f).length = p.length

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).length = p.length

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Iic' {a : α} (ha : (Ioi a).Nonempty) : frontier (Iic a) = {a}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ frontier (Iic a) = {a}

Tactic:
simp [frontier, ha]

Result:
no goals
-- Mathlib/Probability/CDF.lean
lemma cdf_measure_stieltjesFunction (f : StieltjesFunction) (hf0 : Tendsto f atBot (𝓝 0))
    (hf1 : Tendsto f atTop (𝓝 1)) :
    cdf f.measure = f

Proof state:
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
h_prob : IsProbabilityMeasure f.measure
⊢ (cdf f.measure).measure = f.measure

Tactic:
exact measure_cdf f.measure

Result:
no goals

Proof state:
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ (cdf f.measure).measure = f.measure

Tactic:
have h_prob : IsProbabilityMeasure f.measure :=
  ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩

Result:
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
h_prob : IsProbabilityMeasure f.measure
⊢ (cdf f.measure).measure = f.measure

Proof state:
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ f.measure univ = 1

Tactic:
rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]

Result:
no goals

Proof state:
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ cdf f.measure = f

Tactic:
refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0

Result:
f : StieltjesFunction
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ (cdf f.measure).measure = f.measure
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem inf_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f g : A) :
    (f : C(X, ℝ)) ⊓ (g : C(X, ℝ)) ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ ↑f ⊓ ↑g ∈ A.topologicalClosure

Tactic:
rw [inf_eq_half_smul_add_sub_abs_sub' ℝ]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g - |↑g - ↑f|) ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g - |↑g - ↑f|) ∈ A.topologicalClosure

Tactic:
refine
  A.topologicalClosure.smul_mem
    (A.topologicalClosure.sub_mem
      (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
        (A.le_topologicalClosure g.property))
      ?_)
    _

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |↑g - ↑f| ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |↑g - ↑f| ∈ A.topologicalClosure

Tactic:
exact mod_cast abs_mem_subalgebra_closure A _

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem exists_genWeightSpace_zero_le_ker_of_isNoetherian
    [IsNoetherian R M] (x : L) :
    ∃ k : ℕ, genWeightSpace M (0 : L → R) ≤ LinearMap.ker (toEnd R L M x ^ k)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
x : L
⊢ ∃ k, ↑(genWeightSpace M 0) ≤ LinearMap.ker ((toEnd R L M) x ^ k)

Tactic:
simpa using exists_genWeightSpace_le_ker_of_isNoetherian M (0 : L → R) x

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
/-- If `N` is in perfect pairing with `M`, then it is reflexive. -/
lemma isReflexive_of_equiv_dual_of_isReflexive : IsReflexive R N

Proof state:
case bijective_dual_eval'
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑↑(e ≪≫ₗ e.flip.symm.dualMap)

Tactic:
exact LinearEquiv.bijective _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ IsReflexive R N

Tactic:
constructor

Result:
case bijective_dual_eval'
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑(Dual.eval R N)

Proof state:
case bijective_dual_eval'
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
rw [← trans_dualMap_symm_flip e]

Result:
case bijective_dual_eval'
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑↑(e ≪≫ₗ e.flip.symm.dualMap)