harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma transfiniteCompositionsOfShape_le_llp_rlp :
    W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
this : W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
this : W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff] at this

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
this : W.rlp.llp.transfiniteCompositionsOfShape J ≤ W.rlp.llp
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
this : W.rlp.llp.transfiniteCompositionsOfShape J ≤ W.rlp.llp
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
exact le_trans (transfiniteCompositionsOfShape_monotone J W.le_llp_rlp) this

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem support_embDomain_subset {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :
    support (embDomain f x) ⊆ f '' x.support

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : g ∉ ⇑f '' x.support
⊢ g ∉ (embDomain f x).support

Tactic:
rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
⊢ (embDomain f x).support ⊆ ⇑f '' x.support

Tactic:
intro g hg

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : g ∈ (embDomain f x).support
⊢ g ∈ ⇑f '' x.support

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : g ∈ (embDomain f x).support
⊢ g ∈ ⇑f '' x.support

Tactic:
contrapose! hg

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : g ∉ ⇑f '' x.support
⊢ g ∉ (embDomain f x).support
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem Inv1.property [EquivBEq α] {n m : Nat} (x y : α) (map : HashMap α Nat) (hinv : Inv1 n map)
    (hfound1 : map[x]? = some m) (hfound2 : map[y]? = some m) : x = y

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map map✝ : HashMap α Nat
z : α
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hx : (z == x) = true
ih1 : Inv1 m map✝
hy : ¬z = y
hfound2 : map✝[y]? = some m
this : m < m
⊢ x = y

Tactic:
omega

Result:
no goals

Proof state:
case insert
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
n m : Nat
x y : α
map : HashMap α Nat
n✝ : Nat
map✝ : HashMap α Nat
z : α
ih1 : Inv1 n✝ map✝
_ih2 : map✝[z]? = none
ih3 : map✝[x]? = some m → map✝[y]? = some m → x = y
hfound1 : (if (z == x) = true then some n✝ else map✝[x]?) = some m
hfound2 : (if (z == y) = true then some n✝ else map✝[y]?) = some m
⊢ x = y

Tactic:
match hx : z == x with
| false =>
  simp only [beq_eq_false_iff_ne, ne_eq] at hx
  simp only [beq_iff_eq, hx, ↓reduceIte] at hfound1
  match hy : z == y with
  | false =>
    simp only [beq_eq_false_iff_ne, ne_eq] at hy
    simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2
    exact ih3 hfound1 hfound2
  | true =>
    simp only [hy, ↓reduceIte, Option.some.injEq] at hfound2
    have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound1
    omega
| true =>
  simp only [hx, ↓reduceIte, Option.some.injEq] at hfound1
  rcases hfound1 with ⟨rfl⟩
  match hy : z == y with
  | false =>
    simp only [beq_eq_false_iff_ne, ne_eq] at hy
    simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2
    have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound2
    omega
  | true =>
    simp only [beq_iff_eq] at hx hy
    simp only [←hx, hy]

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem toEventualRanges_nonempty (h : F.IsMittagLeffler) [∀ j : J, Nonempty (F.obj j)] (j : J) :
    Nonempty (F.toEventualRanges.obj j)

Proof state:
J : Type u
inst✝² : Category.{u_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j : J
⊢ Nonempty (F.toEventualRanges.obj j)

Tactic:
let ⟨i, f, h⟩ := F.isMittagLeffler_iff_eventualRange.1 h j

Result:
J : Type u
inst✝² : Category.{u_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h✝ : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : F.eventualRange j = range (F.map f)
⊢ Nonempty (F.toEventualRanges.obj j)

Proof state:
J : Type u
inst✝² : Category.{u_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h✝ : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : F.eventualRange j = range (F.map f)
⊢ Nonempty (F.toEventualRanges.obj j)

Tactic:
rw [toEventualRanges_obj, h]

Result:
J : Type u
inst✝² : Category.{u_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h✝ : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : F.eventualRange j = range (F.map f)
⊢ Nonempty ↑(range (F.map f))

Proof state:
J : Type u
inst✝² : Category.{u_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h✝ : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : F.eventualRange j = range (F.map f)
⊢ Nonempty ↑(range (F.map f))

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_of_mem {R : α → β → Prop} {a b ca cb} (ma : a ∈ ca) (mb : b ∈ cb) (ab : R a b) :
    LiftRel R ca cb :=
  ⟨fun {a'} ma' => by rw [mem_unique ma' ma]; exact ⟨b, mb, ab⟩, fun {b'} mb' => by
    rw [mem_unique mb' mb]; exact ⟨a, ma, ab⟩⟩

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a' b

Tactic:
rw [mem_unique ma' ma]

Result:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b

Tactic:
exact ⟨b, mb, ab⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b'

Tactic:
rw [mem_unique mb' mb]

Result:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b

Tactic:
exact ⟨a, ma, ab⟩

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHomMonomial_single_one :
    esymmAlgHomMonomial σ (Finsupp.single i k) 1 = esymm σ R (i + 1) ^ k

Proof state:
σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) 1 = esymm σ R (↑i + 1) ^ k

Tactic:
rw [esymmAlgHomMonomial_single, map_one, one_mul]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_take : ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (take n l₁) (take n l₂)
  | 0, _, _, _ => by simp only [Forall₂.nil, take]
  | _ + 1, _, _, Forall₂.nil => by simp only [Forall₂.nil, take]
  | n + 1, _, _, Forall₂.cons h₁ h₂ => by simp [And.intro h₁ h₂, forall₂_take n]

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
x✝² : List α
x✝¹ : List β
x✝ : Forall₂ R x✝² x✝¹
⊢ Forall₂ R (take 0 x✝²) (take 0 x✝¹)

Tactic:
simp only [Forall₂.nil, take]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
n✝ : ℕ
⊢ Forall₂ R (take (n✝ + 1) []) (take (n✝ + 1) [])

Tactic:
simp only [Forall₂.nil, take]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (take (n + 1) (a✝ :: l₁✝)) (take (n + 1) (b✝ :: l₂✝))

Tactic:
simp [And.intro h₁ h₂, forall₂_take n]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem mem_map_iff {b : β} : b ∈ c.map f ↔ ∃ a, a ∈ c ∧ f a = b :=
  ⟨exists_of_mem_map _, fun h => by
    rcases h with ⟨w, h, h'⟩
    subst b
    apply mem_map c _ h⟩

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
b : β
w : α
h : w ∈ c
h' : f w = b
⊢ b ∈ c.map f

Tactic:
subst b

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
w : α
h : w ∈ c
⊢ f w ∈ c.map f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
b : β
h : ∃ a ∈ c, f a = b
⊢ b ∈ c.map f

Tactic:
rcases h with ⟨w, h, h'⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
b : β
w : α
h : w ∈ c
h' : f w = b
⊢ b ∈ c.map f

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
w : α
h : w ∈ c
⊢ f w ∈ c.map f

Tactic:
apply mem_map c _ h

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem Preadditive.isCoseparating_iff (𝒢 : Set C) :
    IsCoseparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0 :=
  ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [Limits.zero_comp] using hf), fun h𝒢 X Y f g hfg =>
    sub_eq_zero.1 <| h𝒢 _ (by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg)⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h

Tactic:
simpa only [Limits.zero_comp] using hf

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_lt_one {x : ℝ≥0∞} {z : ℝ} (hx : x < 1) (hz : 0 < z) : x ^ z < 1

Proof state:
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : ↑x < 1
⊢ ↑x ^ z < 1

Tactic:
simp only [coe_lt_one_iff] at hx

Result:
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : x < 1
⊢ ↑x ^ z < 1

Proof state:
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : x < 1
⊢ ↑x ^ z < 1

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.rpow_lt_one hx hz]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)

Result:
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : ↑x < 1
⊢ ↑x ^ z < 1
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem _root_.Disjoint.edgeSet {H₁ H₂ : Subgraph G} (h : Disjoint H₁ H₂) :
    Disjoint H₁.edgeSet H₂.edgeSet :=
  disjoint_iff_inf_le.mpr <| by simpa using edgeSet_mono h.le_bot

Proof state:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
h : Disjoint H₁ H₂
⊢ H₁.edgeSet ⊓ H₂.edgeSet ≤ ⊥

Tactic:
simpa using edgeSet_mono h.le_bot

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lintegral_le_of_lmarginal_le [Fintype δ] (s : Finset δ) {f g : (∀ i, π i) → ℝ≥0∞}
    (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ) :
    ∫⁻ x, f x ∂Measure.pi μ ≤ ∫⁻ x, g x ∂Measure.pi μ

Proof state:
case inr.intro
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → π i
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Tactic:
simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_le_of_subset (Finset.subset_univ s) hf hg hfg x]

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Tactic:
rcases isEmpty_or_nonempty (∀ i, π i) with h|⟨⟨x⟩⟩

Result:
case inl
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → π i)
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

case inr.intro
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → π i
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Proof state:
case inl
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → π i)
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Tactic:
simp_rw [lintegral_of_isEmpty, le_rfl]

Result:
no goals
-- Mathlib/Topology/Maps/OpenQuotient.lean
theorem continuousAt_comp_iff (h : IsOpenQuotientMap f) {g : Y → Z} {x : X} :
    ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
h : IsOpenQuotientMap f
g : Y → Z
x : X
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_mul_noncomm (hf : ∀ k, Commute (f <| q.coeff k) x) :
    eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f (q k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }

Tactic:
simp only [← ofFinsupp_mul, eval₂_ofFinsupp]

Result:
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f (q k)) x
⊢ (liftNC ↑f ⇑((powersHom S) x)) (p * q) = (liftNC ↑f ⇑((powersHom S) x)) p * (liftNC ↑f ⇑((powersHom S) x)) q

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f (q k)) x
⊢ (liftNC ↑f ⇑((powersHom S) x)) (p * q) = (liftNC ↑f ⇑((powersHom S) x)) p * (liftNC ↑f ⇑((powersHom S) x)) q

Tactic:
exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
⊢ eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q

Tactic:
rcases p with ⟨p⟩

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
p : R[ℕ]
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
p : R[ℕ]
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q

Tactic:
rcases q with ⟨q⟩

Result:
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f ({ toFinsupp := q }.coeff k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f ({ toFinsupp := q }.coeff k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }

Tactic:
simp only [coeff] at hf

Result:
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f (q k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem IsAlgClosed.isCyclotomicExtension (h : ∀ a ∈ S, NeZero ((a : ℕ) : K)) :
    IsCyclotomicExtension S K K

Proof state:
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
⊢ IsCyclotomicExtension S K K

Tactic:
refine ⟨@fun a ha => ?_, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩

Result:
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑a

Proof state:
case intro
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : (aeval r) (cyclotomic (↑a) K) = 0
⊢ IsPrimitiveRoot r ↑a

Tactic:
haveI := h a ha

Result:
case intro
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : (aeval r) (cyclotomic (↑a) K) = 0
this : NeZero ↑↑a
⊢ IsPrimitiveRoot r ↑a

Proof state:
case intro
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : (aeval r) (cyclotomic (↑a) K) = 0
⊢ ∃ r, IsPrimitiveRoot r ↑a

Tactic:
refine ⟨r, ?_⟩

Result:
case intro
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : (aeval r) (cyclotomic (↑a) K) = 0
⊢ IsPrimitiveRoot r ↑a

Proof state:
case intro
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : (aeval r) (cyclotomic (↑a) K) = 0
this : NeZero ↑↑a
⊢ IsPrimitiveRoot r ↑a

Tactic:
rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr

Result:
no goals

Proof state:
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑a

Tactic:
obtain ⟨r, hr⟩ := IsAlgClosed.exists_aeval_eq_zero K _ (degree_cyclotomic_pos a K a.pos).ne'

Result:
case intro
S : Set ℕ+
K : Type w
inst✝¹ : Field K
inst✝ : IsAlgClosed K
h : ∀ a ∈ S, NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : (aeval r) (cyclotomic (↑a) K) = 0
⊢ ∃ r, IsPrimitiveRoot r ↑a
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem comp_mul_right (hf : IntervalIntegrable f volume a b) (c : ℝ) :
    IntervalIntegrable (fun x => f (x * c)) volume (a / c) (b / c)

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (x * c)) volume (a / c) (b / c)

Tactic:
simpa only [mul_comm] using comp_mul_left hf c

Result:
no goals
-- Mathlib/CategoryTheory/EssentialImage.lean
theorem essSurj_of_surj (h : Function.Surjective F.obj) : EssSurj F where
  mem_essImage Y

Proof state:
case intro
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : Function.Surjective F.obj
X : C
⊢ F.essImage (F.obj X)

Tactic:
apply obj_mem_essImage

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : Function.Surjective F.obj
Y : D
⊢ F.essImage Y

Tactic:
obtain ⟨X, rfl⟩ := h Y

Result:
case intro
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : Function.Surjective F.obj
X : C
⊢ F.essImage (F.obj X)
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem inclusion'_map_eq_top {X : TopCat} (U : Opens X) : (Opens.map U.inclusion').obj U = ⊤

Proof state:
X : TopCat
U : Opens ↑X
⊢ (map U.inclusion').obj U = ⊤

Tactic:
ext1

Result:
case h
X : TopCat
U : Opens ↑X
⊢ ↑((map U.inclusion').obj U) = ↑⊤

Proof state:
case h
X : TopCat
U : Opens ↑X
⊢ ↑((map U.inclusion').obj U) = ↑⊤

Tactic:
exact Subtype.coe_preimage_self _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_eq_sum : p.eval x = p.sum fun e a => a * x ^ e

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ (p.sum fun e a => (RingHom.id R) a * x ^ e) = p.sum fun e a => a * x ^ e

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x p = p.sum fun e a => a * x ^ e

Tactic:
rw [eval, eval₂_eq_sum]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ (p.sum fun e a => (RingHom.id R) a * x ^ e) = p.sum fun e a => a * x ^ e