Theorem: edge_ind_finite_range (RandomGraphs/erdos_renyi.lean)

State before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ Set.Finite (Set.range fun ω => ↑(EdgeInd' (G ω) e))
Tactic:
apply @Set.Finite.subset ℝ {0,1} _ (Set.range fun ω => (EdgeInd' (G ω) e : ℝ)) _
State after:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ Set.Finite {0, 1}

V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}

State before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ Set.Finite {0, 1}

V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
Tactic:
simp only [Set.mem_singleton_iff, zero_ne_one, Set.finite_singleton, Set.Finite.insert]
State after:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}

State before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
Tactic:
simp [EdgeInd']
State after:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => if Edge (G ω) e then 1 else 0) ⊆ {0, 1}

State before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => if Edge (G ω) e then 1 else 0) ⊆ {0, 1}
Tactic:
rintro x ⟨ω, hx⟩
State after:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ x ∈ {0, 1}

State before:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ x ∈ {0, 1}
Tactic:
rw [← hx]
State after:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ (fun ω => if Edge (G ω) e then 1 else 0) ω ∈ {0, 1}

State before:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ (fun ω => if Edge (G ω) e then 1 else 0) ω ∈ {0, 1}
Tactic:
simp only [Set.mem_singleton_iff, zero_ne_one, Set.mem_insert_iff, ite_eq_right_iff, one_ne_zero,
  ite_eq_left_iff]
State after:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ (Edge (G ω) e → False) ∨ (¬Edge (G ω) e → False)

State before:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ (Edge (G ω) e → False) ∨ (¬Edge (G ω) e → False)
Tactic:
exact Classical.em (¬Edge (G ω) e)
State after:
no goals