internlm/Lean-Github huggingface dataset:
Theorem: edge_ind_finite_range
Proof 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]
Proof 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}
Theorem: edge_ind_finite_range
Proof 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]
Proof 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)
Theorem: edge_ind_finite_range
Proof 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)
Proof state after:
no goals
Theorem: expected_edge_count
Proof state before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∫ (ω : Ω), ↑(NumEdges G (_ : ∀ (e : EdgeType V) (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) e) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p
Tactic:
simp only [NumEdges, SimpleFunc.coe_sum, Finset.sum_apply]
Proof state after:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∫ (ω : Ω), ∑ c : EdgeType V, ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) c) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p
Theorem: expected_edge_count
Proof state before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∫ (ω : Ω), ∑ c : EdgeType V, ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) c) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p
Tactic:
rw [integral_finset_sum]
Proof state after:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∑ i : EdgeType V, ∫ (a : Ω), ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) a ∂μ =
    ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Theorem: expected_edge_count
Proof state before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∑ i : EdgeType V, ∫ (a : Ω), ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) a ∂μ =
    ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Tactic:
simp only [bernoulli_expectation (h.bernoulli_edges), Finset.sum_const, Finset.card_univ, Fintype.card, nsmul_eq_mul]
Proof state after:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ↑(Fintype.card (EdgeType V)) * ↑p = ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Theorem: expected_edge_count
Proof state before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ↑(Fintype.card (EdgeType V)) * ↑p = ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Tactic:
rw [Sym2.card_subtype_not_diag, hn]
Proof state after:
case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Theorem: expected_edge_count
Proof state before:
case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Tactic:
simp only [Finset.mem_univ, integrable, forall_true_left, Subtype.forall, implies_true]
Proof state after:
no goals
Theorem: SimpleFunc.coe_prod
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : CommMonoid β
f : ι → SimpleFunc α β
s : Finset ι
⊢ ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
Tactic:
induction s using Finset.cons_induction <;> simp [*]
Proof state after:
no goals
Theorem: SimpleFunc.coe_sum'
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : CommMonoid β
I : Type u_4
f : I → SimpleFunc α ℝ
inst✝ : Fintype I
⊢ ↑(∑ i : I, f i) = ∑ i : I, ↑(f i)
Tactic:
simp only [coe_sum]
Proof state after:
no goals
Theorem: l1_1_3_i
Proof state before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c f : G
h1 : ∀ (g : G), f * g = g
_h2 : ∀ (g : G), g * f = g
⊢ f = 1
Tactic:
rw [← @self_eq_mul_left _ _ _ f, h1]
Proof state after:
no goals
Theorem: l1_1_5_i
Proof state before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
⊢ x * y = x * z → y = z
Tactic:
intro h
Proof state after:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
h : x * y = x * z
⊢ y = z
Theorem: l1_1_5_i
Proof state before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
h : x * y = x * z
⊢ y = z
Tactic:
rwa [← mul_left_cancel_iff]
Proof state after:
no goals
Theorem: l1_1_5_ii
Proof state before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
⊢ x * z = y * z → x = y
Tactic:
intro h
Proof state after:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
h : x * z = y * z
⊢ x = y
Theorem: l1_1_5_ii
Proof state before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c x y z : G
h : x * z = y * z
⊢ x = y
Tactic:
rwa [← mul_right_cancel_iff]
Proof state after:
no goals
Theorem: Ex112.one_mul
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) = a * (a * a⁻¹)
⊢ 1 * a = a
Tactic:
rw [h2, h1] at this
Proof state after:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) = a
⊢ 1 * a = a
Theorem: Ex112.one_mul
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
Tactic:
calc
  a * (a⁻¹ * a) * a⁻¹ = a * a⁻¹ * (a * a⁻¹) := ?_
  _ = a * a⁻¹ * 1 := ?_
  _ = a * 1 * a⁻¹ := ?_
  _ = a * (a * a⁻¹) * a⁻¹ := ?_
Proof state after:
case calc_1
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * (a⁻¹ * a) * a⁻¹ = a * a⁻¹ * (a * a⁻¹)

case calc_2
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * (a * a⁻¹) = a * a⁻¹ * 1

case calc_3
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * 1 = a * 1 * a⁻¹

case calc_4
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * 1 * a⁻¹ = a * (a * a⁻¹) * a⁻¹
Theorem: Ex112.one_mul
Proof state before:
case calc_2
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * (a * a⁻¹) = a * a⁻¹ * 1
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: Ex112.one_mul
Proof state before:
case calc_3
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * 1 = a * 1 * a⁻¹
Tactic:
rw [h1, h1]
Proof state after:
no goals
Theorem: Ex112.one_mul
Proof state before:
case calc_4
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * 1 * a⁻¹ = a * (a * a⁻¹) * a⁻¹
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: Ex112.one_mul
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : (fun x => x * a⁻¹⁻¹) (a * (a⁻¹ * a) * a⁻¹) = (fun x => x * a⁻¹⁻¹) (a * (a * a⁻¹) * a⁻¹)
⊢ a * (a⁻¹ * a) = a * (a * a⁻¹)
Tactic:
simp only at this
Proof state after:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) * a⁻¹ * a⁻¹⁻¹ = a * (a * a⁻¹) * a⁻¹ * a⁻¹⁻¹
⊢ a * (a⁻¹ * a) = a * (a * a⁻¹)
Theorem: Ex112.one_mul
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) = a * (a * a⁻¹)
⊢ a * (a⁻¹ * a) = a * (a * a⁻¹)
Tactic:
exact this
Proof state after:
no goals
Theorem: Ex112.mul_left_inv
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a = 1
Tactic:
calc
  a⁻¹ * a = a⁻¹ * a⁻¹⁻¹ := ?_
  _ = 1 := h2 a⁻¹
Proof state after:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a = a⁻¹ * a⁻¹⁻¹
Theorem: Ex112.mul_left_inv
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a = a⁻¹ * a⁻¹⁻¹
Tactic:
apply congr_arg
Proof state after:
case h
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a = a⁻¹⁻¹
Theorem: Ex112.mul_left_inv
Proof state before:
case h
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a = a⁻¹⁻¹
Tactic:
calc
  a = a * 1 := (h1 a).symm
  _ = a * (a⁻¹ * a⁻¹⁻¹) := by rw [h2]
  _ = a * a⁻¹ * a⁻¹⁻¹ := (Std.Associative.assoc a a⁻¹ a⁻¹⁻¹).symm
  _ = 1 * a⁻¹⁻¹ := by rw [h2]
  _ = a⁻¹⁻¹ := one_mul h1 h2 a⁻¹⁻¹
Proof state after:
no goals
Theorem: Ex112.mul_left_inv
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * 1 = a * (a⁻¹ * a⁻¹⁻¹)
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: Ex112.mul_left_inv
Proof state before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * a⁻¹⁻¹ = 1 * a⁻¹⁻¹
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: Ex113.mul_def
Proof state before:
a b : { z // ‖z‖ = 1 }
⊢ ‖↑a * ↑b‖ = 1
Tactic:
rw [norm_mul, a.prop, b.prop, one_mul]
Proof state after:
no goals
Theorem: Ex113.inv_def
Proof state before:
a : { z // ‖z‖ = 1 }
⊢ ‖(↑a)⁻¹‖ = 1
Tactic:
rw [norm_inv, a.prop, inv_one]
Proof state after:
no goals
Theorem: Ex113.ex1_1_3'
Proof state before:
⊢ {z | ‖z‖ = 1} = {x | ∃ θ, Complex.exp (↑θ * Complex.I) = x}
Tactic:
ext z
Proof state after:
case h
z : ℂ
⊢ z ∈ {z | ‖z‖ = 1} ↔ z ∈ {x | ∃ θ, Complex.exp (↑θ * Complex.I) = x}
Theorem: Ex113.ex1_1_3'
Proof state before:
case h
z : ℂ
⊢ z ∈ {z | ‖z‖ = 1} ↔ z ∈ {x | ∃ θ, Complex.exp (↑θ * Complex.I) = x}
Tactic:
simp only [Complex.norm_eq_abs, Set.mem_setOf_eq, Complex.abs_eq_one_iff]
Proof state after:
no goals
Theorem: l1_2_2_ba'
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (a b : ↥H), ↑(a * b) = ↑a * ↑b) ∧ ↑1 = 1
Tactic:
refine' ⟨_, Subgroup.coe_one _⟩
Proof state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a b : ↥H), ↑(a * b) = ↑a * ↑b
Theorem: l1_2_2_ba'
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a b : ↥H), ↑(a * b) = ↑a * ↑b
Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩
Proof state after:
case mk.mk
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∈ H
b : G
hb : b ∈ H
⊢ ↑({ val := a, property := ha } * { val := b, property := hb }) =
    ↑{ val := a, property := ha } * ↑{ val := b, property := hb }
Theorem: l1_2_2_ba'
Proof state before:
case mk.mk
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∈ H
b : G
hb : b ∈ H
⊢ ↑({ val := a, property := ha } * { val := b, property := hb }) =
    ↑{ val := a, property := ha } * ↑{ val := b, property := hb }
Tactic:
rw [MulMemClass.mk_mul_mk, Subgroup.coe_mk, Subgroup.coe_mk, Subgroup.coe_mk, mul_left_inj]
Proof state after:
no goals
Theorem: l1_2_2_bc
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Set.Nonempty ↑H ∧ ∀ (h₁ h₂ : G), h₁ ∈ ↑H → h₂ ∈ ↑H → h₁ * h₂⁻¹ ∈ ↑H
Tactic:
refine' ⟨⟨1, SetLike.mem_coe.mpr (one_mem _)⟩, fun h₁ h₂ h₁mem h₂mem => _⟩
Proof state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ ↑H
h₂mem : h₂ ∈ ↑H
⊢ h₁ * h₂⁻¹ ∈ ↑H
Theorem: l1_2_2_bc
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ ↑H
h₂mem : h₂ ∈ ↑H
⊢ h₁ * h₂⁻¹ ∈ ↑H
Tactic:
rw [SetLike.mem_coe] at h₁mem h₂mem ⊢
Proof state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ H
h₂mem : h₂ ∈ H
⊢ h₁ * h₂⁻¹ ∈ H
Theorem: l1_2_2_bc
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ H
h₂mem : h₂ ∈ H
⊢ h₁ * h₂⁻¹ ∈ H
Tactic:
exact Subgroup.mul_mem _ h₁mem (Subgroup.inv_mem _ h₂mem)
Proof state after:
no goals
Theorem: l1_2_3_2
Proof state before:
n : ℤ
⊢ ↑(ex1232 n) = {k | n ∣ k}
Tactic:
ext
Proof state after:
case h
n x✝ : ℤ
⊢ x✝ ∈ ↑(ex1232 n) ↔ x✝ ∈ {k | n ∣ k}
Theorem: l1_2_3_2
Proof state before:
case h
n x✝ : ℤ
⊢ x✝ ∈ ↑(ex1232 n) ↔ x✝ ∈ {k | n ∣ k}
Tactic:
simp [ex1232, Int.mem_zmultiples_iff]
Proof state after:
no goals
Theorem: n1_2_5'
Proof state before:
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ↑(Subgroup.closure X) = {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
simp only [Subgroup.closure, Subgroup.coe_sInf]
Proof state after:
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s = {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Theorem: n1_2_5'
Proof state before:
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s = {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
apply subset_antisymm
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s ⊆ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}

case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x} ⊆ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s ⊆ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
intro x hx
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
simp only [Set.mem_iInter] at hx
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
Tactic:
simp only [Set.mem_setOf]
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
Tactic:
specialize hx (n125 X) _
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ n125 X ∈ {K | X ⊆ ↑K}

case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ↑(n125 X)
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ↑(n125 X)
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
Tactic:
simpa [n125] using hx
Proof state after:
no goals
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ n125 X ∈ {K | X ⊆ ↑K}
Tactic:
intro y hy
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ y ∈ ↑(n125 X)
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ y ∈ ↑(n125 X)
Tactic:
simp only [n125, Set.mem_setOf, Subgroup.coe_set_mk]
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ ∃ x ∈ n125Set X, List.prod x = y
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ ∃ x ∈ n125Set X, List.prod x = y
Tactic:
refine' ⟨[y], _, List.prod_singleton⟩
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ [y] ∈ n125Set X
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ [y] ∈ n125Set X
Tactic:
simp only [hy, n125Set, forall_eq, true_or_iff, Set.mem_setOf, List.mem_singleton,
  Set.mem_union]
Proof state after:
no goals
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
⊢ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x} ⊆ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Tactic:
intro x hx
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ {x | ∃ x_1 ∈ n125Set X, List.prod x_1 = x}
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Tactic:
simp only [Set.mem_setOf, n125Set] at hx
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
Tactic:
simp only [Set.mem_iInter, SetLike.mem_coe]
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ ∀ i ∈ {K | X ⊆ ↑K}, x ∈ i
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ ∀ i ∈ {K | X ⊆ ↑K}, x ∈ i
Tactic:
intro i hi
Proof state after:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
⊢ x ∈ i
Theorem: n1_2_5'
Proof state before:
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
⊢ x ∈ i
Tactic:
obtain ⟨y, h1, rfl⟩ := hx
Proof state after:
case a.intro.intro
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y : List G
h1 : ∀ x ∈ y, x ∈ X ∪ X⁻¹
⊢ List.prod y ∈ i
Theorem: n1_2_5'
Proof state before:
case a.intro.intro.nil
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
h1 : ∀ x ∈ [], x ∈ X ∪ X⁻¹
⊢ List.prod [] ∈ i
Tactic:
simp only [List.prod_nil, one_mem]
Proof state after:
no goals