harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Distributions/Uniform.lean
theorem hasPDF {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
    (hu : IsUniform X s ℙ μ) : HasPDF X ℙ μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ Measure.map X ℙ = μ.withDensity (t.indicator ((μ t)⁻¹ • 1))

Tactic:
rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
  withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ HasPDF X ℙ μ

Tactic:
apply hasPDF_of_map_eq_withDensity (hu.aemeasurable hns hnt) (t.indicator ((μ t)⁻¹ • 1)) <|
  (measurable_one.aemeasurable.const_smul (μ t)⁻¹).indicator (measurableSet_toMeasurable μ s)

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ Measure.map X ℙ = μ.withDensity (t.indicator ((μ t)⁻¹ • 1))

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
⊢ HasPDF X ℙ μ

Tactic:
let t := toMeasurable μ s

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ HasPDF X ℙ μ
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_add_eq_add_tsub (hb : AddLECancellable b) (h : b ≤ a) :
    a - b + c = a + c - b

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

Tactic:
rw [add_comm a, hb.add_tsub_assoc_of_le h, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Expr.eq_of_toPoly_eq (ctx : Context) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx

Proof state:
ctx : Context
a b : Expr
h✝ : (a.toPoly == b.toPoly) = true
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b

Tactic:
assumption

Result:
no goals

Proof state:
ctx : Context
a b : Expr
h✝ : (a.toPoly == b.toPoly) = true
h : Poly.denote ctx a.toPoly = Poly.denote ctx b.toPoly
⊢ denote ctx a = denote ctx b

Tactic:
simp [toPoly_denote] at h

Result:
ctx : Context
a b : Expr
h✝ : (a.toPoly == b.toPoly) = true
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b

Proof state:
ctx : Context
a b : Expr
h : (a.toPoly == b.toPoly) = true
⊢ denote ctx a = denote ctx b

Tactic:
have h := congrArg (Poly.denote ctx) (eq_of_beq h)

Result:
ctx : Context
a b : Expr
h✝ : (a.toPoly == b.toPoly) = true
h : Poly.denote ctx a.toPoly = Poly.denote ctx b.toPoly
⊢ denote ctx a = denote ctx b
-- Mathlib/Probability/Integration.lean
theorem lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace
    {Mf Mg mΩ : MeasurableSpace Ω} {μ : Measure Ω} (hMf : Mf ≤ mΩ) (hMg : Mg ≤ mΩ)
    (h_ind : Indep Mf Mg μ) (h_meas_f : Measurable[Mf] f) (h_meas_g : Measurable[Mg] g) :
    ∫⁻ ω, f ω * g ω ∂μ = (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, g ω ∂μ

Proof state:
case h_iSup
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∫⁻ (ω : Ω), ⨆ i, f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ n, f' n ω ∂μ

Tactic:
rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', ENNReal.mul_iSup]

Result:
case h_iSup
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ⨆ n, ∫⁻ (a : Ω), f a * f' n a ∂μ = ⨆ i, (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ

case h_iSup.hf
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∀ (n : ℕ), Measurable fun ω => f ω * f' n ω

case h_iSup.h_mono
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ Monotone fun i ω => f ω * f' i ω

Proof state:
Ω : Type u_1
f g : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_meas_g : Measurable g
⊢ ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
revert g

Result:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
⊢ ∀ {g : Ω → ℝ≥0∞}, Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_isStoppingTime [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι]
    [Countable ι] [TopologicalSpace β] [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β]
    {f : Filtration ι m} {u : ι → Ω → β} {s : Set β} {n n' : ι} (hu : Adapted f u)
    (hs : MeasurableSet s) : IsStoppingTime f (hitting u s n n')

Proof state:
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
h_set_eq_Union : {ω | hitting u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}

Tactic:
rw [h_set_eq_Union]

Result:
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
h_set_eq_Union : {ω | hitting u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s
⊢ MeasurableSet (⋃ j ∈ Set.Icc n i, u j ⁻¹' s)

Proof state:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : ConditionallyCompleteLinearOrder ι
inst✝⁵ : WellFoundedLT ι
inst✝⁴ : Countable ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
h_le : ∀ (ω : Ω), hitting u s n n' ω ≤ i
⊢ MeasurableSet {ω | hitting u s n n' ω ≤ i}

Tactic:
simp [h_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem det_ne_zero [Nontrivial R] (g : SpecialLinearGroup n R) : det ↑ₘg ≠ 0

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ (↑g).det ≠ 0

Tactic:
rw [g.det_coe]

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 0
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem NormedSpace.equicontinuous_TFAE : List.TFAE
    [ EquicontinuousAt ((↑) ∘ f) 0,
      Equicontinuous ((↑) ∘ f),
      UniformEquicontinuous ((↑) ∘ f),
      ∃ C, ∀ i x, ‖f i x‖ ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ i x, ‖f i x‖ ≤ C * ‖x‖,
      ∃ C, ∀ i, ‖f i‖ ≤ C,
      ∃ C ≥ 0, ∀ i, ‖f i‖ ≤ C,
      BddAbove (Set.range (‖f ·‖)),
      (⨆ i, (‖f i‖₊ : ENNReal)) < ⊤ ]

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖,
      ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖),
      ⨆ i, ↑‖f i‖₊ < ⊤].TFAE

Tactic:
tfae_have 7 ↔ 8 := by
  simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x => ‖f x‖)
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖,
      ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖),
      ⨆ i, ↑‖f i‖₊ < ⊤].TFAE
-- Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
theorem equivalence₁CounitIso_eq : (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{u_6, u_1} A
inst✝¹ : Category.{u_7, u_2} A'
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y : B'
⊢ (equivalence₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y

Tactic:
simp [equivalence₁, equivalence₀]

Result:
no goals

Proof state:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{u_6, u_1} A
inst✝¹ : Category.{u_7, u_2} A'
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

Tactic:
ext Y

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{u_6, u_1} A
inst✝¹ : Category.{u_7, u_2} A'
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y : B'
⊢ (equivalence₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_eq_univ_iff {c : Set (Set α)} : ⋃₀ c = univ ↔ ∀ a, ∃ b ∈ c, a ∈ b

Proof state:
α : Type u_1
c : Set (Set α)
⊢ ⋃₀ c = univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b

Tactic:
simp only [eq_univ_iff_forall, mem_sUnion]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- `m` is `n`-smooth if and only if all prime divisors of `m` are less than `n`. -/
lemma mem_smoothNumbers' {n m : ℕ} : m ∈ smoothNumbers n ↔ ∀ p, p.Prime → p ∣ m → p < n

Proof state:
n m : ℕ
⊢ m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Prime p → p ∣ m → p < n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers', Finset.mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findM?_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
    as.toList.findM? p = as.findM? p

Proof state:
case mk
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
toList✝ : List α
⊢ List.findM? p { toList := toList✝ }.toList = findM? p { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ List.findM? p as.toList = findM? p as

Tactic:
cases as

Result:
case mk
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
toList✝ : List α
⊢ List.findM? p { toList := toList✝ }.toList = findM? p { toList := toList✝ }
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_eq_comm : xᶜ = y ↔ yᶜ = x

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ = y ↔ yᶜ = x

Tactic:
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) :
    choose n k = n ! / (k ! * (n - k)!)

Proof state:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)

Tactic:
exact (mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm

Result:
no goals

Proof state:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n ! / (k ! * (n - k)!)

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]

Result:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)
-- Mathlib/CategoryTheory/IsConnected.lean
theorem nat_trans_from_is_connected [IsPreconnected J] {X Y : C}
    (α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y) :
    ∀ j j' : J, α.app j = (α.app j' : X ⟶ Y) :=
  @constant_of_preserves_morphisms _ _ _ (X ⟶ Y) (fun j => α.app j) fun _ _ f => by
    have := α.naturality f
    erw [id_comp, comp_id] at this
    exact this.symm

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝

Tactic:
have := α.naturality f

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : ((Functor.const J).obj X).map f ≫ α.app x✝ = α.app x✝¹ ≫ ((Functor.const J).obj Y).map f
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : α.app x✝ = α.app x✝¹
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝

Tactic:
exact this.symm

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : ((Functor.const J).obj X).map f ≫ α.app x✝ = α.app x✝¹ ≫ ((Functor.const J).obj Y).map f
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝

Tactic:
erw [id_comp, comp_id] at this

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
this : α.app x✝ = α.app x✝¹
⊢ (fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem prod_X_sub_C_nextCoeff {s : Finset ι} (f : ι → R) :
    nextCoeff (∏ i ∈ s, (X - C (f i))) = -∑ i ∈ s, f i

Proof state:
R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
⊢ (∏ i ∈ s, (X - C (f i))).nextCoeff = -∑ i ∈ s, f i

Tactic:
simpa using multiset_prod_X_sub_C_nextCoeff (s.1.map f)

Result:
no goals
-- Mathlib/Topology/Irreducible.lean
theorem irreducibleComponents_eq_maximals_closed (X : Type*) [TopologicalSpace X] :
    irreducibleComponents X = { s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s}

Proof state:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
x : Set X
h : IsIrreducible x
e : s ≤ x
this : closure x ≤ s
⊢ x ≤ s

Tactic:
exact le_trans subset_closure this

Result:
no goals

Proof state:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s} → s ∈ irreducibleComponents X

Tactic:
intro H

Result:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
⊢ s ∈ irreducibleComponents X

Proof state:
case h.mp
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X → s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

Tactic:
intro H

Result:
case h.mp
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

Proof state:
case h
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X ↔ s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

Tactic:
constructor

Result:
case h.mp
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X → s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s} → s ∈ irreducibleComponents X

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
⊢ irreducibleComponents X = {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

Tactic:
ext s

Result:
case h
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X ↔ s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

Proof state:
case h.mp
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}

Tactic:
exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩

Result:
no goals

Proof state:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
x : Set X
h : IsIrreducible x
e : s ≤ x
⊢ x ≤ s

Tactic:
have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)

Result:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
x : Set X
h : IsIrreducible x
e : s ≤ x
this : closure x ≤ s
⊢ x ≤ s

Proof state:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
⊢ s ∈ irreducibleComponents X

Tactic:
refine ⟨H.1.2, fun x h e => ?_⟩

Result:
case h.mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
x : Set X
h : IsIrreducible x
e : s ≤ x
⊢ x ≤ s
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_insert_right [DecidableEq β] :
    image₂ f s (insert b t) = (s.image fun a => f a b) ∪ image₂ f s t :=
  coe_injective <| by
    push_cast
    exact image2_insert_right

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (insert b t)) = ↑(image (fun a => f a b) s ∪ image₂ f s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (insert b ↑t) = (fun a => f a b) '' ↑s ∪ image2 f ↑s ↑t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (insert b ↑t) = (fun a => f a b) '' ↑s ∪ image2 f ↑s ↑t

Tactic:
exact image2_insert_right

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem UCompactlyGeneratedSpace.isClosed [UCompactlyGeneratedSpace.{u} X] {s : Set X}
    (hs : ∀ (S : CompHaus.{u}) (f : C(S, X)), IsClosed (f ⁻¹' s)) : IsClosed s

Proof state:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsClosed
      (Sigma.mk i ⁻¹'
        ((fun x =>
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s))

Tactic:
exact fun ⟨S, f⟩ ↦ hs S f

Result:
no goals

Proof state:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed s

Tactic:
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isClosed_coinduced,
  isClosed_sigma_iff]

Result:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsClosed
      (Sigma.mk i ⁻¹'
        ((fun x =>
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s))
-- Mathlib/RingTheory/Ideal/IsPrincipal.lean
theorem associatesNonZeroDivisorsEquivIsPrincipal_mul (x y : Associates R⁰) :
    (associatesNonZeroDivisorsEquivIsPrincipal R (x * y) : Ideal R) =
      (associatesNonZeroDivisorsEquivIsPrincipal R x) *
        (associatesNonZeroDivisorsEquivIsPrincipal R y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates ↥R⁰
⊢ ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) (x * y)) =
    ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x) * ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) y)

Tactic:
simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, _root_.map_mul, Submonoid.coe_mul,
  associatesEquivIsPrincipal_mul]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem mul_left_dvd (hu : IsUnit u) : u * a ∣ b ↔ a ∣ b

Proof state:
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b

Tactic:
apply Units.mul_left_dvd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b