harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sym/Card.lean
theorem card_subtype_diag [Fintype α] : card { a : Sym2 α // a.IsDiag } = card α

Proof state:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ x.IsDiag

Tactic:
rw [mem_filter, univ_product_univ, mem_image]

Result:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Proof state:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // a.IsDiag } = #(image Sym2.mk univ.diag)

Tactic:
rw [← filter_image_mk_isDiag, Fintype.card_of_subtype]

Result:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ x.IsDiag

Proof state:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Tactic:
obtain ⟨a, ha⟩ := Quot.exists_rep x

Result:
case h.e'_2.H.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Proof state:
case h.e'_2.H.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Tactic:
exact and_iff_right ⟨a, mem_univ _, ha⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // a.IsDiag } = Fintype.card α

Tactic:
convert card_image_diag (univ : Finset α)

Result:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // a.IsDiag } = #(image Sym2.mk univ.diag)

Proof state:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ x.IsDiag

Tactic:
rintro x

Result:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ x.IsDiag
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_pow_apply_head (x : α) (l : List α) (h : Nodup (x :: l)) (n : ℕ) :
    (formPerm (x :: l) ^ n) x =
      (x :: l)[(n % (x :: l).length)]'(Nat.mod_lt _ (Nat.zero_lt_succ _))

Proof state:
case h.e'_3.h.e'_7.h.e'_5
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ n = 0 + n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ ((x :: l).formPerm ^ n) x = (x :: l)[n % (x :: l).length]

Tactic:
convert formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)

Result:
case h.e'_3.h.e'_7.h.e'_5
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ n = 0 + n
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
lemma MeasurableSet.of_union_range_cover (hi₁ : MeasurableEmbedding i₁)
    (hi₂ : MeasurableEmbedding i₂) (h : univ ⊆ range i₁ ∪ range i₂)
    (hs₁ : MeasurableSet (i₁ ⁻¹' s)) (hs₂ : MeasurableSet (i₂ ⁻¹' s)) : MeasurableSet s

Proof state:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ MeasurableSet s

Tactic:
convert (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂)

Result:
case h.e'_3
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ s = i₁ '' (i₁ ⁻¹' s) ∪ i₂ '' (i₂ ⁻¹' s)

Proof state:
case h.e'_3
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ s = i₁ '' (i₁ ⁻¹' s) ∪ i₂ '' (i₂ ⁻¹' s)

Tactic:
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right,univ_subset_iff.1 h]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_self (n : ℕ) : dist n n = 0

Proof state:
n : ℕ
⊢ n.dist n = 0

Tactic:
simp [dist, tsub_self]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma le_liminf_add : (liminf u f) + (liminf v f) ≤ liminf (u + v) f

Proof state:
case h
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
exact c_ab.trans (add_lt_add a_x b_x)

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
⊢ ∀ᶠ (a : α) in f, c < (u + v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x

Result:
case h
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Result:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
⊢ ∀ᶠ (a : α) in f, c < (u + v) a
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjOpcyclesSelfIso_inv_naturality :
    opcyclesMap ((single C c j).map f) j ≫ (singleObjOpcyclesSelfIso c j B).inv =
      (singleObjOpcyclesSelfIso c j A).inv ≫ f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ opcyclesMap ((single C c j).map f) j ≫ (singleObjOpcyclesSelfIso c j B).inv = (singleObjOpcyclesSelfIso c j A).inv ≫ f

Tactic:
rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
  comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1S_add (T : Set α → E →L[ℝ] F) (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (f g : α →₁ₛ[μ] E) :
    setToL1S T (f + g) = setToL1S T f + setToL1S T g

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)

Tactic:
rw [← SimpleFunc.setToSimpleFunc_add T h_add (SimpleFunc.integrable f)
    (SimpleFunc.integrable g)]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ setToL1S T (f + g) = setToL1S T f + setToL1S T g

Tactic:
simp_rw [setToL1S]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) =
    SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)

Tactic:
exact
  SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _)
    (add_toSimpleFunc f g)

Result:
no goals
-- Mathlib/RingTheory/IsPrimary.lean
lemma isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul :
    S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 →
      ∃ n : ℕ, r ^ n • (⊤ : Submodule R (M ⧸ S)) = ⊥

Proof state:
case a.h.h.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝ ∉ S → a✝¹ • a✝ ∈ S → ∃ n, a✝¹ ^ n • ⊤ = ⊥

Tactic:
rw [forall_comm, ← or_iff_not_imp_left,
  ← LinearMap.range_eq_top.mpr S.mkQ_surjective, ← map_top]

Result:
case a.h.h.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ = ⊥

Proof state:
case a.h.h.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ = ⊥

Tactic:
simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔ ∀ (r : R), ∀ x ∉ S, r • x ∈ S → ∃ n, r ^ n • ⊤ = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
refine (and_congr_right fun _ ↦ ?_)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔ ∀ (r : R), ∀ x ∉ S, r • x ∈ S → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
congr! 2

Result:
case a.h.h.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝ ∉ S → a✝¹ • a✝ ∈ S → ∃ n, a✝¹ ^ n • ⊤ = ⊥
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_hom (e : F ≅ G) (n : A) : e.hom.hom n ≫ e.inv.hom n = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
⊢ e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)

Tactic:
rw [← comp_hom, e.hom_inv_id, id_hom]

Result:
no goals
-- Mathlib/Data/Finset/PImage.lean
theorem toFinset_some {a : α} [Decidable (some a).Dom] : (some a).toFinset = {a}

Proof state:
α : Type u_1
a : α
inst✝ : Decidable (some a).Dom
⊢ (some a).toFinset = {a}

Tactic:
simp [toFinset]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.comp_continuous {g : β → γ} {f : α → β} {s : Set β} (hg : ContinuousOn g s)
    (hf : Continuous f) (hs : ∀ x, f x ∈ s) : Continuous (g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : Continuous f
hs : ∀ (x : α), f x ∈ s
⊢ Continuous (g ∘ f)

Tactic:
rw [continuous_iff_continuousOn_univ] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : ContinuousOn f univ
hs : ∀ (x : α), f x ∈ s
⊢ ContinuousOn (g ∘ f) univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : ContinuousOn f univ
hs : ∀ (x : α), f x ∈ s
⊢ ContinuousOn (g ∘ f) univ

Tactic:
exact hg.comp hf fun x _ => hs x

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_eq_singleton_iff : Icc a b = {c} ↔ a = c ∧ b = c

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_le_neg_add_cancel (x : PGame) : 0 ≤ -x + x

Proof state:
x : PGame
⊢ 0 ≤ -x + x

Tactic:
rw [← neg_le_neg_iff, neg_zero]

Result:
x : PGame
⊢ -(-x + x) ≤ 0

Proof state:
x : PGame
⊢ -(-x + x) ≤ 0

Tactic:
exact neg_add_le.trans (neg_add_cancel_le_zero _)

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
lemma measurableSet_lt (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g) :
    MeasurableSet[m] {a | f a < g a}

Proof state:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a < g a}

Tactic:
simpa only [lt_iff_le_not_le] using (hf.measurableSet_le hg).inter (hg.measurableSet_le hf).compl

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem isPreconnected_connectedComponentIn {x : α} {F : Set α} :
    IsPreconnected (connectedComponentIn F x)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅)

Tactic:
split_ifs

Result:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ IsPreconnected (Subtype.val '' connectedComponent ⟨x, h✝⟩)

case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ IsPreconnected ∅

Proof state:
case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ IsPreconnected ∅

Tactic:
exact isPreconnected_empty

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ IsPreconnected (Subtype.val '' connectedComponent ⟨x, h✝⟩)

Tactic:
exact IsInducing.subtypeVal.isPreconnected_image.mpr isPreconnected_connectedComponent

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (connectedComponentIn F x)

Tactic:
rw [connectedComponentIn]

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅)
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma counitForward_val_snd (s : CostructuredArrow yoneda A) (x : F.obj (op s)) :
    (counitForward F s x).val.snd = F.map (eqToHom (by simp [← CostructuredArrow.eq_mk])) x :=
  YonedaCollection.mk_snd _ _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ op s = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F s x).val))

Tactic:
simp [← CostructuredArrow.eq_mk]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem one_div_mul_eq_div : 1 / a * b = b / a

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ 1 / a * b = b / a

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_add_left (μ κ : Kernel α β) (η : Kernel (α × β) γ)
    [IsSFiniteKernel μ] [IsSFiniteKernel κ] :
    (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
a✝ : α
s✝ : Set (β × γ)
hs : MeasurableSet s✝
⊢ (((μ + κ) ⊗ₖ η) a✝) s✝ = ((μ ⊗ₖ η + κ ⊗ₖ η) a✝) s✝

Tactic:
simp [compProd_apply hs]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
simp [hη]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
ext _ _ hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
a✝ : α
s✝ : Set (β × γ)
hs : MeasurableSet s✝
⊢ (((μ + κ) ⊗ₖ η) a✝) s✝ = ((μ ⊗ₖ η + κ ⊗ₖ η) a✝) s✝

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
by_cases hη : IsSFiniteKernel η

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel μ
inst✝ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
-- Mathlib/Order/Cover.lean
lemma exists_covBy_of_wellFoundedLT [wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬ IsMax a) :
    ∃ a', a ⋖ a'

Proof state:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedLT α
a : α
h : ∃ b, a < b
⊢ ∃ a', a ⋖ a'

Tactic:
exact ⟨_, wellFounded_lt.min_mem _ h, fun a' ↦ wf.wf.not_lt_min _ h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedLT α
a : α
h : ¬IsMax a
⊢ ∃ a', a ⋖ a'

Tactic:
rw [not_isMax_iff] at h

Result:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedLT α
a : α
h : ∃ b, a < b
⊢ ∃ a', a ⋖ a'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_flatten' (f : β → α → β) (b : β) (L : Array (Array α))
    (w : stop = L.flatten.size) :
    (flatten L).foldl f b 0 stop = L.foldl (fun b l => l.foldl f b) b

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
b : β
L : Array (Array α)
⊢ foldl f b L.flatten = foldl (fun b l => foldl f b l) b L

Tactic:
cases L using array₂_induction

Result:
case of
β : Type u_1
α : Type u_2
f : β → α → β
b : β
xss✝ : List (List α)
⊢ foldl f b (List.map List.toArray xss✝).toArray.flatten =
    foldl (fun b l => foldl f b l) b (List.map List.toArray xss✝).toArray

Proof state:
case of
β : Type u_1
α : Type u_2
f : β → α → β
b : β
xss✝ : List (List α)
⊢ foldl f b (List.map List.toArray xss✝).toArray.flatten =
    foldl (fun b l => foldl f b l) b (List.map List.toArray xss✝).toArray

Tactic:
simp [List.foldl_flatten, List.foldl_map]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
stop : Nat
f : β → α → β
b : β
L : Array (Array α)
w : stop = L.flatten.size
⊢ foldl f b L.flatten 0 stop = foldl (fun b l => foldl f b l) b L

Tactic:
subst w

Result:
β : Type u_1
α : Type u_2
f : β → α → β
b : β
L : Array (Array α)
⊢ foldl f b L.flatten = foldl (fun b l => foldl f b l) b L
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (insertMany empty l).1.get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (empty.insertMany l).val.get! k' = cast ⋯ v

Tactic:
rw [get!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean
theorem complex_d_comp (n : ℕ) :
    I.cocomplex.d n (n + 1) ≫ I.cocomplex.d (n + 1) (n + 2) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ I.cocomplex.d n (n + 1) ≫ I.cocomplex.d (n + 1) (n + 2) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem zero_testAgainstNN_apply (f : Ω →ᵇ ℝ≥0) : (0 : FiniteMeasure Ω).testAgainstNN f = 0

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0

Tactic:
simp only [testAgainstNN, toMeasure_zero, lintegral_zero_measure, ENNReal.zero_toNNReal]

Result:
no goals