internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * (a * x) = a⁻¹ * (a * y)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * (a * y) = a⁻¹ * a * y
Tactic:
rw [← mul_assoc]
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * a * y = 1 * y
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ 1 * y = y
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_one
Proof state before:
A : Type ?u.7038
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a * 1 = a
Tactic:
apply mul_left_cancel (a := a⁻¹)
Proof state after:
A : Type ?u.7038
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a⁻¹ * (a * 1) = a⁻¹ * a
Theorem: Tutorial.mul_one
Proof state before:
A : Type ?u.7038
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a⁻¹ * (a * 1) = a⁻¹ * a
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_inv_self
Proof state before:
A : Type ?u.9053
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Tactic:
apply mul_left_cancel (a := a⁻¹)
Proof state after:
A : Type ?u.9053
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a⁻¹ * (a * a⁻¹) = a⁻¹ * 1
Theorem: Tutorial.mul_inv_self
Proof state before:
A : Type ?u.9053
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a⁻¹ * (a * a⁻¹) = a⁻¹ * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_inv_cancel_left
Proof state before:
A : Type ?u.10914
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * (a⁻¹ * b) = b
Tactic:
rw [← mul_assoc]
Proof state after:
A : Type ?u.10914
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * a⁻¹ * b = b
Theorem: Tutorial.mul_inv_cancel_left
Proof state before:
A : Type ?u.10914
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * a⁻¹ * b = b
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_inv_cancel_right
Proof state before:
A : Type ?u.12143
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b * b⁻¹ = a
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_right
Proof state before:
A : Type ?u.13426
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ * b = a
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
⊢ x * a = y * a → x = y
Tactic:
intro h
Proof state after:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ x = y
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ x = y
Tactic:
calc
  x = x * 1 := by simp
  _ = x * (a * a⁻¹) := by simp
  _ = (x * a) * a⁻¹ := by rw [← mul_assoc]
  _ = (y * a) * a⁻¹ := by rw [h]
  _ = y * (a * a⁻¹) := by rw [mul_assoc]
  _ = y * 1 := by simp
  _ = y := by simp
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ x = x * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ x * 1 = x * (a * a⁻¹)
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ x * (a * a⁻¹) = x * a * a⁻¹
Tactic:
rw [← mul_assoc]
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ x * a * a⁻¹ = y * a * a⁻¹
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ y * a * a⁻¹ = y * (a * a⁻¹)
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ y * (a * a⁻¹) = y * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.14883
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : x * a = y * a
⊢ y * 1 = y
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.inv_eq_of_mul_eq_one_left
Proof state before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
⊢ x * a = 1 → a⁻¹ = x
Tactic:
intro h
Proof state after:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ = x
Theorem: Tutorial.inv_eq_of_mul_eq_one_left
Proof state before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ = x
Tactic:
apply mul_right_cancel a
Proof state after:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = x * a
Theorem: Tutorial.inv_eq_of_mul_eq_one_left
Proof state before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = x * a
Tactic:
rw [h]
Proof state after:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = 1
Theorem: Tutorial.inv_eq_of_mul_eq_one_left
Proof state before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.inv_one
Proof state before:
A : Type ?u.18067
G : Type
inst✝¹ : Ring A
inst✝ : Group G
⊢ 1⁻¹ = 1
Tactic:
apply inv_eq_of_mul_eq_one_left
Proof state after:
case a
A : Type ?u.18067
G : Type
inst✝¹ : Ring A
inst✝ : Group G
⊢ 1 * 1 = 1
Theorem: Tutorial.inv_one
Proof state before:
case a
A : Type ?u.18067
G : Type
inst✝¹ : Ring A
inst✝ : Group G
⊢ 1 * 1 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.inv_inv
Proof state before:
A : Type ?u.18884
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a⁻¹⁻¹ = a
Tactic:
apply inv_eq_of_mul_eq_one_left
Proof state after:
case a
A : Type ?u.18884
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Theorem: Tutorial.inv_inv
Proof state before:
case a
A : Type ?u.18884
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_inv_rev
Proof state before:
A : Type ?u.19458
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
apply inv_eq_of_mul_eq_one_left
Proof state after:
case a
A : Type ?u.19458
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ b⁻¹ * a⁻¹ * (a * b) = 1
Theorem: Tutorial.mul_inv_rev
Proof state before:
case a
A : Type ?u.19458
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ b⁻¹ * a⁻¹ * (a * b) = 1
Tactic:
rw [← mul_assoc]
Proof state after:
case a
A : Type ?u.19458
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ b⁻¹ * a⁻¹ * a * b = 1
Theorem: Tutorial.mul_inv_rev
Proof state before:
case a
A : Type ?u.19458
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ b⁻¹ * a⁻¹ * a * b = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
⊢ a * b⁻¹ = c ↔ a = c * b
Tactic:
constructor
Proof state after:
case mp
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
⊢ a * b⁻¹ = c → a = c * b

case mpr
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
⊢ a = c * b → a * b⁻¹ = c
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
case mp
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
⊢ a * b⁻¹ = c → a = c * b
Tactic:
intro h
Proof state after:
case mp
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a = c * b
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
case mp
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a = c * b
Tactic:
apply mul_right_cancel (a := b⁻¹)
Proof state after:
case mp
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a * b⁻¹ = c * b * b⁻¹
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
case mp
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a * b⁻¹ = c * b * b⁻¹
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
case mpr
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
⊢ a = c * b → a * b⁻¹ = c
Tactic:
intro h
Proof state after:
case mpr
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
case mpr
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c
Tactic:
rw [h]
Proof state after:
case mpr
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a = c * b
⊢ c * b * b⁻¹ = c
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
case mpr
A : Type ?u.20667
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
h : a = c * b
⊢ c * b * b⁻¹ = c
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_inv_eq_one
Proof state before:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = b
Tactic:
suffices a * b⁻¹ = 1 ↔ a = 1 * b by simpa using this
Proof state after:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = 1 * b
Theorem: Tutorial.mul_inv_eq_one
Proof state before:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = 1 * b
Tactic:
exact mul_inv_eq_iff_eq_mul
Proof state after:
no goals
Theorem: Tutorial.mul_inv_eq_one
Proof state before:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
this : a * b⁻¹ = 1 ↔ a = 1 * b
⊢ a * b⁻¹ = 1 ↔ a = b
Tactic:
simpa using this
Proof state after:
no goals
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 ↔ a = b
Tactic:
constructor
Proof state after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 → a = b

case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a = b → a⁻¹ * b = 1
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 → a = b
Tactic:
intro h
Proof state after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a⁻¹ * b = 1
⊢ a = b
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a⁻¹ * b = 1
⊢ a = b
Tactic:
have h : a⁻¹ * b⁻¹⁻¹ = 1 := by simp [h]
Proof state after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ * b⁻¹⁻¹ = 1
⊢ a = b
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ * b⁻¹⁻¹ = 1
⊢ a = b
Tactic:
rw [mul_inv_eq_one] at h
Proof state after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
⊢ a = b
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
⊢ a = b
Tactic:
suffices a⁻¹⁻¹ = b⁻¹⁻¹ by simpa using this
Proof state after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
⊢ a⁻¹⁻¹ = b⁻¹⁻¹
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
⊢ a⁻¹⁻¹ = b⁻¹⁻¹
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a⁻¹ * b = 1
⊢ a⁻¹ * b⁻¹⁻¹ = 1
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
this : a⁻¹⁻¹ = b⁻¹⁻¹
⊢ a = b
Tactic:
simpa using this
Proof state after:
no goals
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a = b → a⁻¹ * b = 1
Tactic:
intro h
Proof state after:
case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a = b
⊢ a⁻¹ * b = 1
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a = b
⊢ a⁻¹ * b = 1
Tactic:
rw [h]
Proof state after:
case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a = b
⊢ b⁻¹ * b = 1
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a = b
⊢ b⁻¹ * b = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.Subgroup.inv_mem_iff
Proof state before:
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H ↔ a ∈ H
Tactic:
constructor
Proof state after:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H → a ∈ H

case mpr
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a ∈ H → a⁻¹ ∈ H
Theorem: Tutorial.Subgroup.inv_mem_iff
Proof state before:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H → a ∈ H
Tactic:
intro h
Proof state after:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h : a⁻¹ ∈ H
⊢ a ∈ H
Theorem: Tutorial.Subgroup.inv_mem_iff
Proof state before:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h : a⁻¹ ∈ H
⊢ a ∈ H
Tactic:
have h := inv_mem h
Proof state after:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h✝ : a⁻¹ ∈ H
h : a⁻¹⁻¹ ∈ H
⊢ a ∈ H
Theorem: Tutorial.Subgroup.inv_mem_iff
Proof state before:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h✝ : a⁻¹ ∈ H
h : a⁻¹⁻¹ ∈ H
⊢ a ∈ H
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Tutorial.Subgroup.inv_mem_iff
Proof state before:
case mpr
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a ∈ H → a⁻¹ ∈ H
Tactic:
exact inv_mem
Proof state after:
no goals
Theorem: Tutorial.inv_smul_smul
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ a⁻¹ • a • x = x
Tactic:
rw [smul_smul]
Proof state after:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ (a⁻¹ * a) • x = x
Theorem: Tutorial.inv_smul_smul
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ (a⁻¹ * a) • x = x
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.smul_inv_smul
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ a • a⁻¹ • x = x
Tactic:
rw [smul_smul]
Proof state after:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ (a * a⁻¹) • x = x
Theorem: Tutorial.smul_inv_smul
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ (a * a⁻¹) • x = x
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.GroupAction.injective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = y
Tactic:
calc x = a⁻¹ • a • x := by rw [inv_smul_smul]
  _ = a⁻¹ • a • y := by rw [h]
  _ = y := by rw [inv_smul_smul]
Proof state after:
no goals
Theorem: Tutorial.GroupAction.injective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = a⁻¹ • a • x
Tactic:
rw [inv_smul_smul]
Proof state after:
no goals
Theorem: Tutorial.GroupAction.injective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ a⁻¹ • a • x = a⁻¹ • a • y
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Tutorial.GroupAction.injective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ a⁻¹ • a • y = y
Tactic:
rw [inv_smul_smul]
Proof state after:
no goals
Theorem: Tutorial.GroupAction.surjective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
⊢ Function.Surjective fun x => a • x
Tactic:
intro y
Proof state after:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ ∃ a_1, (fun x => a • x) a_1 = y
Theorem: Tutorial.GroupAction.surjective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ ∃ a_1, (fun x => a • x) a_1 = y
Tactic:
use a⁻¹ • y
Proof state after:
case h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ (fun x => a • x) (a⁻¹ • y) = y
Theorem: Tutorial.GroupAction.surjective
Proof state before:
case h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ (fun x => a • x) (a⁻¹ • y) = y
Tactic:
exact smul_inv_smul
Proof state after:
no goals
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y ↔ y ∈ orbit G x
Tactic:
constructor
Proof state after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y → y ∈ orbit G x

case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ y ∈ orbit G x → orbit G x = orbit G y
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y → y ∈ orbit G x
Tactic:
intro h
Proof state after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G x
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G x
Tactic:
rw [h]
Proof state after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G y
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G y
Tactic:
exists 1
Proof state after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ 1 • y = y
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ 1 • y = y
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ y ∈ orbit G x → orbit G x = orbit G y
Tactic:
intro ⟨a, ha⟩
Proof state after:
case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
⊢ orbit G x = orbit G y
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
⊢ orbit G x = orbit G y
Tactic:
ext z
Proof state after:
case mpr.h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x ↔ z ∈ orbit G y
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x ↔ z ∈ orbit G y
Tactic:
constructor
Proof state after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x → z ∈ orbit G y

case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G y → z ∈ orbit G x
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x → z ∈ orbit G y
Tactic:
intro ⟨b, hb⟩
Proof state after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ z ∈ orbit G y
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ z ∈ orbit G y
Tactic:
rw [← hb, ← ha]
Proof state after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ b • x ∈ orbit G (a • x)
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ b • x ∈ orbit G (a • x)
Tactic:
exists b * a⁻¹
Proof state after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ (b * a⁻¹) • a • x = b • x
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ (b * a⁻¹) • a • x = b • x
Tactic:
simp [mul_smul]
Proof state after:
no goals
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G y → z ∈ orbit G x
Tactic:
intro ⟨b, hb⟩
Proof state after:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ z ∈ orbit G x
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ z ∈ orbit G x
Tactic:
rw [← hb, ← ha]
Proof state after:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ b • a • x ∈ orbit G x
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ b • a • x ∈ orbit G x
Tactic:
exists b * a
Proof state after:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ (b * a) • x = b • a • x
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ (b * a) • x = b • a • x
Tactic:
simp [mul_smul]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_const
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
⊢ (fun x => c - c - (x - a) * 0) =o[𝓝 a] fun x => x - a
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_id
Proof state before:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ (fun x => id x - id a - (x - a) * 1) =o[𝓝 a] fun x => x - a
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.add
Proof state before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x + g x - (f a + g a) - (x - a) * (f' + g')) = fun x =>
    f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')
Tactic:
case eq1 =>
  funext x
  ring
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.add
Proof state before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply IsLittleO.add hf hg
Proof state after:
no goals