internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - (nestedInterval U n).1 - (c - (nestedInterval U n).1)| ≤
    |x - (nestedInterval U n).1| + |c - (nestedInterval U n).1|
Tactic:
apply abs_sub
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - (nestedInterval U n).1| + |c - (nestedInterval U n).1| =
    x - (nestedInterval U n).1 + (c - (nestedInterval U n).1)
Tactic:
apply congrArg₂ <;> rw [abs_eq_self] <;> linarith
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ x - (nestedInterval U n).1 + (c - (nestedInterval U n).1) < ε / 2 + ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
Proof state after:
no goals
Theorem: Tutorial.Category.Initial.uniq'
Proof state before:
C : Type u
inst✝ : Category C
a : C
h : Initial a
b : C
f g : Hom a b
⊢ f = h.fromInitial b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Category.Initial.uniq'
Proof state before:
C : Type u
inst✝ : Category C
a : C
h : Initial a
b : C
f g : Hom a b
⊢ h.fromInitial b = g
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Injective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
hf : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
apply hfinj
Proof state after:
case a
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
hf : f x₁ = f x₂
⊢ f x₁ = f x₂
Theorem: Tutorial.Injective.comp
Proof state before:
case a
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
hf : f x₁ = f x₂
⊢ f x₁ = f x₂
Tactic:
apply hf
Proof state after:
no goals
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
have h : g (f x₁) = g (f x₂) := by
   rw [hf]
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ x₁ = x₂
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ x₁ = x₂
Tactic:
apply hgfinj
Proof state after:
case a
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ (g ∘ f) x₁ = (g ∘ f) x₂
Theorem: Tutorial.Injective.of_comp
Proof state before:
case a
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ (g ∘ f) x₁ = (g ∘ f) x₂
Tactic:
simp
Proof state after:
case a
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ g (f x₁) = g (f x₂)
Theorem: Tutorial.Injective.of_comp
Proof state before:
case a
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ g (f x₁) = g (f x₂)
Tactic:
apply h
Proof state after:
no goals
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ g (f x₁) = g (f x₂)
Tactic:
rw [hf]
Proof state after:
no goals
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Tactic:
have ⟨x, hx⟩ := hfsurj y
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
x : X
hx : f x = y
⊢ ∃ x, (g ∘ f) x = z
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
x : X
hx : f x = y
⊢ ∃ x, (g ∘ f) x = z
Tactic:
exists x
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
x : X
hx : f x = y
⊢ (g ∘ f) x = z
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
x : X
hx : f x = y
⊢ (g ∘ f) x = z
Tactic:
simp
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
x : X
hx : f x = y
⊢ g (f x) = z
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
x : X
hx : f x = y
⊢ g (f x) = z
Tactic:
rw [hx, hy]
Proof state after:
no goals
Theorem: Tutorial.Surjective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
⊢ Surjective g
Tactic:
intro z
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
⊢ ∃ x, g x = z
Theorem: Tutorial.Surjective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
⊢ ∃ x, g x = z
Tactic:
have ⟨x, hx⟩ := h z
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
x : X
hx : (g ∘ f) x = z
⊢ ∃ x, g x = z
Theorem: Tutorial.Surjective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
x : X
hx : (g ∘ f) x = z
⊢ ∃ x, g x = z
Tactic:
exists f x
Proof state after:
no goals
Theorem: Tutorial.map_one
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
⊢ f 1 = 1
Tactic:
have h : f 1 * f 1 = f 1 * 1 := by
  rw [← map_mul, mul_one, mul_one]
Proof state after:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
h : f 1 * f 1 = f 1 * 1
⊢ f 1 = 1
Theorem: Tutorial.map_one
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
h : f 1 * f 1 = f 1 * 1
⊢ f 1 = 1
Tactic:
exact mul_left_cancel _ h
Proof state after:
no goals
Theorem: Tutorial.map_one
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
⊢ f 1 * f 1 = f 1 * 1
Tactic:
rw [← map_mul, mul_one, mul_one]
Proof state after:
no goals
Theorem: Tutorial.map_inv
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
a : G₁
⊢ f a⁻¹ = (f a)⁻¹
Tactic:
apply eq_inv_of_mul_eq_one_left
Proof state after:
case a
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
a : G₁
⊢ f a⁻¹ * f a = 1
Theorem: Tutorial.map_inv
Proof state before:
case a
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
a : G₁
⊢ f a⁻¹ * f a = 1
Tactic:
rw [← map_mul, inv_mul_self, map_one]
Proof state after:
no goals
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Injective ⇑f → ∀ (a : G₁), f a = 1 → a = 1
Tactic:
intro hf a ha
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ a = 1
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ a = 1
Tactic:
apply hf
Proof state after:
case mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ f a = f 1
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ f a = f 1
Tactic:
rw [ha, map_one]
Proof state after:
no goals
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → Function.Injective ⇑f
Tactic:
intro h a b hab
Proof state after:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a b : G₁
hab : f a = f b
⊢ a = b
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a b : G₁
hab : f a = f b
⊢ a = b
Tactic:
rw [← mul_inv_eq_one] at *
Proof state after:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ a * b⁻¹ = 1
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ a * b⁻¹ = 1
Tactic:
apply h
Proof state after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 1
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 1
Tactic:
rw [map_mul, map_inv, hab]
Proof state after:
no goals
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ → ∀ (a : G₁), f a = 1 → a = 1
Tactic:
intro h a (hf : a ∈ f.ker)
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ker f = ⊥
a : G₁
hf : a ∈ ker f
⊢ a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ker f = ⊥
a : G₁
hf : a ∈ ker f
⊢ a = 1
Tactic:
simpa [h] using hf
Proof state after:
no goals
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → ker f = ⊥
Tactic:
intro h
Proof state after:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
⊢ ker f = ⊥
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
⊢ ker f = ⊥
Tactic:
ext a
Proof state after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a ∈ ker f ↔ a ∈ ⊥
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a ∈ ker f ↔ a ∈ ⊥
Tactic:
simp only [mem_ker, mem_bot]
Proof state after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 ↔ a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 ↔ a = 1
Tactic:
constructor
Proof state after:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 → a = 1

case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a = 1 → f a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 → a = 1
Tactic:
intro ha
Proof state after:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ a = 1
Tactic:
apply h
Proof state after:
case mpr.a.mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ f a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a.mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ f a = 1
Tactic:
apply ha
Proof state after:
no goals
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a = 1 → f a = 1
Tactic:
intro ha
Proof state after:
case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : a = 1
⊢ f a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : a = 1
⊢ f a = 1
Tactic:
rw [ha, map_one]
Proof state after:
no goals
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ ∃ a, f a = y
Tactic:
have hy : y ∈ (⊤ : Subgroup G₂) := by
  simp
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ ⊤
⊢ ∃ a, f a = y
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ ⊤
⊢ ∃ a, f a = y
Tactic:
rw [← hrange] at hy
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
⊢ ∃ a, f a = y
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
⊢ ∃ a, f a = y
Tactic:
have ⟨x, hx⟩ := hy
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
x : G₁
hx : f x = y
⊢ ∃ a, f a = y
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
x : G₁
hx : f x = y
⊢ ∃ a, f a = y
Tactic:
exists x
Proof state after:
no goals
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ y ∈ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
⊢ range f = ⊤
Tactic:
ext y
Proof state after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ y ∈ range f ↔ y ∈ ⊤
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ y ∈ range f ↔ y ∈ ⊤
Tactic:
simp only [mem_range, mem_top, iff_true]
Proof state after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ ∃ a, f a = y
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ ∃ a, f a = y
Tactic:
apply hsurj y
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = 1
Tactic:
calc
  a = a * 1 := by simp
  _ = (homToPerm G a) 1 := by
    rfl
    _ = 1 := by
    simp [h]
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a * 1 = ((homToPerm G) a) 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ ((homToPerm G) a) 1 = 1
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Geometry.triangle_rotate
Proof state before:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ ¬collinear p q r → ¬collinear q r p
Tactic:
simp[collinear]
Proof state after:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ (∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x) → ∀ (x : line P), q ∈ x → r ∈ x → ¬p ∈ x
Theorem: Geometry.triangle_rotate
Proof state before:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ (∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x) → ∀ (x : line P), q ∈ x → r ∈ x → ¬p ∈ x
Tactic:
intro triangle_pqr l hq hr hp
Proof state after:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x
l : line P
hq : q ∈ l
hr : r ∈ l
hp : p ∈ l
⊢ False
Theorem: Geometry.triangle_rotate
Proof state before:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x
l : line P
hq : q ∈ l
hr : r ∈ l
hp : p ∈ l
⊢ False
Tactic:
apply triangle_pqr <;> assumption
Proof state after:
no goals
Theorem: Geometry.quadrangle_rotate
Proof state before:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ isQuadrangle p q r s → isQuadrangle q r s p
Tactic:
intro ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ isQuadrangle q r s p
Theorem: Geometry.quadrangle_rotate
Proof state before:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ isQuadrangle q r s p
Tactic:
exact ⟨triangle_qrs, triangle_rotate triangle_pqr, triangle_rotate triangle_pqs, triangle_rotate triangle_prs⟩
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_left
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ (p q : P), p ∈ p ⊔ q
Tactic:
intro p q
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
⊢ p ∈ p ⊔ q
Theorem: ProjectivePlane.connectingLine_left
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
⊢ p ∈ p ⊔ q
Tactic:
exact (Exists.choose_spec (exists_connecting_line p q)).left
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_right
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ (p q : P), q ∈ p ⊔ q
Tactic:
intro p q
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
⊢ q ∈ p ⊔ q
Theorem: ProjectivePlane.connectingLine_right
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
⊢ q ∈ p ⊔ q
Tactic:
exact (Exists.choose_spec (exists_connecting_line p q)).right
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ {p q : P} {l : line P}, p ≠ q → p ∈ l → q ∈ l → l = p ⊔ q
Tactic:
intro p q l hpq hpl hql
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
⊢ l = p ⊔ q
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
⊢ l = p ⊔ q
Tactic:
let m := p ⊔ q
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
⊢ l = p ⊔ q
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
⊢ l = p ⊔ q
Tactic:
have hpm : p ∈ m := by simp
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
⊢ l = p ⊔ q
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
⊢ l = p ⊔ q
Tactic:
have hqm : q ∈ m := by simp
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
hqm : q ∈ m
⊢ l = p ⊔ q
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
hqm : q ∈ m
⊢ l = p ⊔ q
Tactic:
have h : p = q ∨ l = m := point_line_uniq hpl hql hpm hqm
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
hqm : q ∈ m
h : p = q ∨ l = m
⊢ l = p ⊔ q
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
hqm : q ∈ m
h : p = q ∨ l = m
⊢ l = p ⊔ q
Tactic:
cases h with
| inl hpq' => contradiction
| inr h' => assumption
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
⊢ p ∈ m
Tactic:
simp
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
⊢ q ∈ m
Tactic:
simp
Proof state after:
no goals