internlm/Lean-Github huggingface dataset:
Theorem: Polynomial.natDegree_discConv_le
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ ((algebraMap S R) (w r) • P.comp (X + C r)).natDegree ≤ P.natDegree
Tactic:
refine (natDegree_smul_le _ _).trans ?_
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (P.comp (X + C r)).natDegree ≤ P.natDegree
Theorem: Polynomial.natDegree_discConv_le
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (P.comp (X + C r)).natDegree ≤ P.natDegree
Tactic:
simp [natDegree_comp]
Proof state after:
no goals
Theorem: Polynomial.degree_discConv_le
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w P).degree ≤ P.degree
Tactic:
obtain rfl | hP := eq_or_ne P 0
Proof state after:
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w 0).degree ≤ degree 0

case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ (discConv w P).degree ≤ P.degree
Theorem: Polynomial.degree_discConv_le
Proof state before:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ (discConv w P).degree ≤ P.degree
Tactic:
refine degree_le_natDegree.trans $ (Nat.cast_le.2 natDegree_discConv_le).trans ?_
Proof state after:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ ↑P.natDegree ≤ P.degree
Theorem: Polynomial.degree_discConv_le
Proof state before:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hP : P ≠ 0
⊢ ↑P.natDegree ≤ P.degree
Tactic:
rw [degree_eq_natDegree hP]
Proof state after:
no goals
Theorem: Polynomial.degree_discConv_le
Proof state before:
case inl
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w 0).degree ≤ degree 0
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.degree_discConv_lt
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
⊢ (discConv w P).degree < P.degree
Tactic:
have := coeff_discConv_natDegree w P
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = (w.sum fun x => id) • P.leadingCoeff
⊢ (discConv w P).degree < P.degree
Theorem: Polynomial.degree_discConv_lt
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = (w.sum fun x => id) • P.leadingCoeff
⊢ (discConv w P).degree < P.degree
Tactic:
rw [hw, zero_smul] at this
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ (discConv w P).degree < P.degree
Theorem: Polynomial.degree_discConv_lt
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ (discConv w P).degree < P.degree
Tactic:
refine' (degree_sum_le _ _).trans_lt $ (Finset.sup_lt_iff _).2 _
Proof state after:
case refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ⊥ < P.degree

case refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree
Theorem: Polynomial.degree_discConv_lt
Proof state before:
case refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ⊥ < P.degree

case refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree
Tactic:
sorry
Proof state after:
case refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree
Theorem: Polynomial.degree_discConv_lt
Proof state before:
case refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree
Tactic:
sorry
Proof state after:
no goals
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1
Tactic:
have :
  ((univ : Finset β) : Set β).PairwiseDisjoint fun b ↦
    univ.filter fun a : α ↦ g a = b := by
  refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _
  simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
  exact hb (ha₁.symm.trans ha₂)
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1
Tactic:
rw [← sum_disjiUnion _ _ this]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ x ∈ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this, f x = 1
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ x ∈ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this, f x = 1
Tactic:
convert h
Proof state after:
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this = univ
Theorem: PMF.map_ofFintype
Proof state before:
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this = univ
Tactic:
exact eq_univ_of_forall fun a ↦
  mem_disjiUnion.2 ⟨_, mem_univ _, mem_filter.2 ⟨mem_univ _, rfl⟩⟩
Proof state after:
no goals
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
Tactic:
refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₁
ha₂ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₂
⊢ False
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₁
ha₂ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₂
⊢ False
Tactic:
simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : g a = b₁
ha₂ : g a = b₂
⊢ False
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : g a = b₁
ha₂ : g a = b₂
⊢ False
Tactic:
exact hb (ha₁.symm.trans ha₂)
Proof state after:
no goals
Theorem: PMF.map_ofFintype
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ map g (ofFintype f h) = ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) ⋯
Tactic:
ext b : 1
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (map g (ofFintype f h)) b = (ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) ⋯) b
Theorem: PMF.map_ofFintype
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (map g (ofFintype f h)) b = (ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) ⋯) b
Tactic:
simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0
Theorem: PMF.map_ofFintype
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0
Tactic:
exact tsum_eq_sum fun _ h ↦ (h $ mem_univ _).elim
Proof state after:
no goals
Theorem: PMF.map_toMeasure
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : PMF α
hf : Measurable f
⊢ Measure.map f p.toMeasure = (map f p).toMeasure
Tactic:
ext s hs : 1
Proof state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s
Theorem: PMF.map_toMeasure
Proof state before:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s
Tactic:
rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]
Proof state after:
no goals
Theorem: PMF.support_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b✝ b : Prop
⊢ b ∈ (bernoulli' p hp).support ↔ b ∈ {b | if b then p ≠ 0 else p ≠ 1}
Tactic:
by_cases b <;> simp [*, hp.lt_iff_ne, tsub_eq_zero_iff_le]
Proof state after:
no goals
Theorem: PMF.mem_support_bernoulli'_iff
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
⊢ b ∈ (bernoulli' p hp).support ↔ if b then p ≠ 0 else p ≠ 1
Tactic:
simp
Proof state after:
no goals
Theorem: PMF.map_not_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
⊢ map Not (bernoulli' p hp) = bernoulli' (1 - p) ⋯
Tactic:
have : ∀ p : Prop, (Finset.univ.filter fun q : Prop ↦ ¬ q ↔ p) = {¬ p} := by
  rintro p
  ext q
  by_cases p <;> by_cases q <;> simp [*]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ map Not (bernoulli' p hp) = bernoulli' (1 - p) ⋯
Theorem: PMF.map_not_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ map Not (bernoulli' p hp) = bernoulli' (1 - p) ⋯
Tactic:
refine' (map_ofFintype _ _ _).trans _
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => (¬a) = b) Finset.univ, if a then ↑p else 1 - ↑p) ⋯ =
    bernoulli' (1 - p) ⋯
Theorem: PMF.map_not_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => (¬a) = b) Finset.univ, if a then ↑p else 1 - ↑p) ⋯ =
    bernoulli' (1 - p) ⋯
Tactic:
simp only [this, bernoulli', Finset.mem_filter, Finset.mem_univ, true_and_iff,
  Finset.mem_disjiUnion, tsub_le_self, eq_iff_iff, Finset.sum_singleton, WithTop.coe_sub,
  ENNReal.coe_one]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ ofFintype (fun b => if ¬b then ↑p else 1 - ↑p) ⋯ = ofFintype (fun b => if b then ↑(1 - p) else 1 - ↑(1 - p)) ⋯
Theorem: PMF.map_not_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
⊢ ofFintype (fun b => if ¬b then ↑p else 1 - ↑p) ⋯ = ofFintype (fun b => if b then ↑(1 - p) else 1 - ↑(1 - p)) ⋯
Tactic:
congr 1 with q
Proof state after:
case e_f.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
q : Prop
⊢ (if ¬q then ↑p else 1 - ↑p) = if q then ↑(1 - p) else 1 - ↑(1 - p)
Theorem: PMF.map_not_bernoulli'
Proof state before:
case e_f.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
q : Prop
⊢ (if ¬q then ↑p else 1 - ↑p) = if q then ↑(1 - p) else 1 - ↑(1 - p)
Tactic:
split_ifs <;> simp [ENNReal.sub_sub_cancel WithTop.one_ne_top (ENNReal.coe_le_coe.2 hp)]
Proof state after:
no goals
Theorem: PMF.map_not_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
⊢ ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
Tactic:
rintro p
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p : Prop
⊢ Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
Theorem: PMF.map_not_bernoulli'
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p : Prop
⊢ Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
Tactic:
ext q
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p q : Prop
⊢ q ∈ Finset.filter (fun q => ¬q ↔ p) Finset.univ ↔ q ∈ {¬p}
Theorem: PMF.map_not_bernoulli'
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p✝ : ℝ≥0
hp : p✝ ≤ 1
b p q : Prop
⊢ q ∈ Finset.filter (fun q => ¬q ↔ p) Finset.univ ↔ q ∈ {¬p}
Tactic:
by_cases p <;> by_cases q <;> simp [*]
Proof state after:
no goals
Theorem: SimpleGraph.Subgraph.map_id
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H : SimpleGraph V
G : SimpleGraph α
G' : G.Subgraph
⊢ Subgraph.map Hom.id G' = G'
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: SimpleGraph.Subgraph.map_comp
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
G' : G.Subgraph
f : G →g H
g : H →g I
⊢ Subgraph.map (g.comp f) G' = Subgraph.map g (Subgraph.map f G')
Tactic:
ext <;> simp [Subgraph.map]
Proof state after:
no goals
Theorem: SimpleGraph.Subgraph.edgeSet_map
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
⊢ (Subgraph.map f G').edgeSet = Sym2.map ⇑f '' G'.edgeSet
Tactic:
ext e
Proof state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
e : Sym2 β
⊢ e ∈ (Subgraph.map f G').edgeSet ↔ e ∈ Sym2.map ⇑f '' G'.edgeSet
Theorem: SimpleGraph.Subgraph.edgeSet_map
Proof state before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
e : Sym2 β
⊢ e ∈ (Subgraph.map f G').edgeSet ↔ e ∈ Sym2.map ⇑f '' G'.edgeSet
Tactic:
induction' e using Sym2.ind with a b
Proof state after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ s(a, b) ∈ (Subgraph.map f G').edgeSet ↔ s(a, b) ∈ Sym2.map ⇑f '' G'.edgeSet
Theorem: SimpleGraph.Subgraph.edgeSet_map
Proof state before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ s(a, b) ∈ (Subgraph.map f G').edgeSet ↔ s(a, b) ∈ Sym2.map ⇑f '' G'.edgeSet
Tactic:
simp only [mem_edgeSet, Sym2.exists, Relation.Map, and_or_left, exists_or, map_adj,
  Set.mem_image, Sym2.map_pair_eq, Sym2.eq, Sym2.rel_iff]
Proof state after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ↔
    (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∨ ∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a
Theorem: SimpleGraph.Subgraph.edgeSet_map
Proof state before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ↔
    (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∨ ∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a
Tactic:
refine' (or_iff_left_of_imp _).symm
Proof state after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a) → ∃ a_2 b_1, G'.Adj a_2 b_1 ∧ f a_2 = a ∧ f b_1 = b
Theorem: SimpleGraph.Subgraph.edgeSet_map
Proof state before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a) → ∃ a_2 b_1, G'.Adj a_2 b_1 ∧ f a_2 = a ∧ f b_1 = b
Tactic:
rintro ⟨a, b, hab, rfl, rfl⟩
Proof state after:
case h.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : α
hab : G'.Adj a b
⊢ ∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = f b ∧ f b_1 = f a
Theorem: SimpleGraph.Subgraph.edgeSet_map
Proof state before:
case h.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : α
hab : G'.Adj a b
⊢ ∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = f b ∧ f b_1 = f a
Tactic:
exact ⟨b, a, hab.symm, rfl, rfl⟩
Proof state after:
no goals
Theorem: SimpleGraph.Subgraph.edgeSet_coe
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet
Tactic:
ext e
Proof state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Theorem: SimpleGraph.Subgraph.edgeSet_coe
Proof state before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Tactic:
induction' e using Sym2.ind with a b
Proof state after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : ↑G'.verts
⊢ s(a, b) ∈ G'.coe.edgeSet ↔ s(a, b) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Theorem: SimpleGraph.Subgraph.edgeSet_coe
Proof state before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : ↑G'.verts
⊢ s(a, b) ∈ G'.coe.edgeSet ↔ s(a, b) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Tactic:
simp
Proof state after:
no goals