awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)
have simp : SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
Tactic: simp only [zpow_negSucc, inv_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
⊢ x = 1 ↔ y = 1
have rw : a * x * a⁻¹ = 1 ↔ y = 1
Tactic: rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
rw : a * x * a⁻¹ = 1 ↔ y = 1
⊢ x = 1 ↔ y = 1
have rw₁ : y * a * a⁻¹ = 1 ↔ y = 1
Tactic: rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
rw : a * x * a⁻¹ = 1 ↔ y = 1
rw₁ : y * a * a⁻¹ = 1 ↔ y = 1
⊢ x = 1 ↔ y = 1
have rw₂ : y = 1 ↔ y = 1
Tactic: rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
have rw : a * x * x' = y * y' * a
Tactic: rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
rw : a * x * x' = y * y' * a
⊢ a * (x * x') = y * y' * a
have rw₁ : y * a * x' = y * y' * a
Tactic: rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
rw : a * x * x' = y * y' * a
rw₁ : y * a * x' = y * y' * a
⊢ a * (x * x') = y * y' * a
have rw₂ : y * (a * x') = y * y' * a
Tactic: rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
rw : a * x * x' = y * y' * a
rw₁ : y * a * x' = y * y' * a
rw₂ : y * (a * x') = y * y' * a
⊢ a * (x * x') = y * y' * a
have rw₃ : y * (y' * a) = y * y' * a
Tactic: rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
rw : a * x * x' = y * y' * a
rw₁ : y * a * x' = y * y' * a
rw₂ : y * (a * x') = y * y' * a
rw₃ : y * (y' * a) = y * y' * a
⊢ a * (x * x') = y * y' * a
have rw₄ : y * y' * a = y * y' * a
Tactic: rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)
have rw : a * (b * x) = z * (a * b)
Tactic: rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
rw : a * (b * x) = z * (a * b)
⊢ a * b * x = z * (a * b)
have rw₁ : a * (y * b) = z * (a * b)
Tactic: rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
rw : a * (b * x) = z * (a * b)
rw₁ : a * (y * b) = z * (a * b)
⊢ a * b * x = z * (a * b)
have rw₂ : a * y * b = z * (a * b)
Tactic: rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
rw : a * (b * x) = z * (a * b)
rw₁ : a * (y * b) = z * (a * b)
rw₂ : a * y * b = z * (a * b)
⊢ a * b * x = z * (a * b)
have rw₃ : z * a * b = z * (a * b)
Tactic: rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
S : Type u_1
inst : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
rw : a * (b * x) = z * (a * b)
rw₁ : a * (y * b) = z * (a * b)
rw₂ : a * y * b = z * (a * b)
rw₃ : z * a * b = z * (a * b)
⊢ a * b * x = z * (a * b)
have rw₄ : z * (a * b) = z * (a * b)
Tactic: rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
a : M
⊢ SemiconjBy a 1 1
have rw : a * 1 = 1 * a
Tactic: rw [SemiconjBy, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
a : M
rw : a * 1 = 1 * a
⊢ SemiconjBy a 1 1
have rw₁ : a = 1 * a
Tactic: rw [SemiconjBy, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
a : M
rw : a * 1 = 1 * a
rw₁ : a = 1 * a
⊢ SemiconjBy a 1 1
have rw₂ : a = a
Tactic: rw [SemiconjBy, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (HPow.hPow (β := ℕ) x 0) (HPow.hPow (β := ℕ) y 0)
have zero : SemiconjBy a 1 1
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
have succ : SemiconjBy a (x ^ n * x) (y ^ n * y)
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)
have zero : SemiconjBy a (HPow.hPow (β := ℕ) x 0) (HPow.hPow (β := ℕ) y 0)
Tactic: induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
zero : SemiconjBy a (HPow.hPow (β := ℕ) x 0) (HPow.hPow (β := ℕ) y 0)
⊢ SemiconjBy a (x ^ n) (y ^ n)
have succ : ∀ (n : ℕ) (ih : SemiconjBy a (x ^ n) (y ^ n)), SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
Tactic: induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a
have rw : a * x = a * x * (a⁻¹ * a)
Tactic: rw [mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x : G
rw : a * x = a * x * (a⁻¹ * a)
⊢ a * x = a * x * a⁻¹ * a
have rw₁ : a * x = a * x * 1
Tactic: rw [mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x : G
rw : a * x = a * x * (a⁻¹ * a)
rw₁ : a * x = a * x * 1
⊢ a * x = a * x * a⁻¹ * a
have rw₂ : a * x = a * x
Tactic: rw [mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * a * b⁻¹ * (b * x * b⁻¹) = b * y * b⁻¹ * (b * a * b⁻¹) ↔ a * x = y * a
have simp : b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a
Tactic: simp only [← mul_assoc, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a
have rw : b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a
have rw : b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a
have rw : b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a
have rw : b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a
have repeat : b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
Tactic: repeat rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
have rw : a * (x * b⁻¹) = y * (a * b⁻¹) ↔ a * x = y * a
Tactic: rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : a * (x * b⁻¹) = y * (a * b⁻¹) ↔ a * x = y * a
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
have rw₁ : a * x * b⁻¹ = y * (a * b⁻¹) ↔ a * x = y * a
Tactic: rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : a * (x * b⁻¹) = y * (a * b⁻¹) ↔ a * x = y * a
rw₁ : a * x * b⁻¹ = y * (a * b⁻¹) ↔ a * x = y * a
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
have rw₂ : a * x * b⁻¹ = y * a * b⁻¹ ↔ a * x = y * a
Tactic: rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : a * (x * b⁻¹) = y * (a * b⁻¹) ↔ a * x = y * a
rw₁ : a * x * b⁻¹ = y * (a * b⁻¹) ↔ a * x = y * a
rw₂ : a * x * b⁻¹ = y * a * b⁻¹ ↔ a * x = y * a
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
have rw₃ : a * x = y * a ↔ a * x = y * a
Tactic: rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y
have rw : SemiconjBy a y y
Tactic: rw [h, SemiconjBy, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : CancelCommMonoid M
a x y : M
h : x = y
rw : SemiconjBy a y y
⊢ SemiconjBy a x y
have rw₁ : a * y = y * a
Tactic: rw [h, SemiconjBy, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Defs (goal)
Goal:
M : Type u_2
inst : CancelCommMonoid M
a x y : M
h : x = y
rw : SemiconjBy a y y
rw₁ : a * y = y * a
⊢ SemiconjBy a x y
have rw₂ : y * a = y * a
Tactic: rw [h, SemiconjBy, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
⊢ a * (↑x⁻¹ : M) = (↑y⁻¹ : M) * ((↑y : M) * a) * (↑x⁻¹ : M)
have rw : a * (↑x⁻¹ : M) = a * (↑x⁻¹ : M)
Tactic: rw [Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
⊢ (↑y⁻¹ : M) * ((↑y : M) * a) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
have rw : (↑y⁻¹ : M) * (a * (↑x : M)) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
Tactic: rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
rw : (↑y⁻¹ : M) * (a * (↑x : M)) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
⊢ (↑y⁻¹ : M) * ((↑y : M) * a) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
have rw₁ : (↑y⁻¹ : M) * (a * (↑x : M) * (↑x⁻¹ : M)) = (↑y⁻¹ : M) * a
Tactic: rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
rw : (↑y⁻¹ : M) * (a * (↑x : M)) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
rw₁ : (↑y⁻¹ : M) * (a * (↑x : M) * (↑x⁻¹ : M)) = (↑y⁻¹ : M) * a
⊢ (↑y⁻¹ : M) * ((↑y : M) * a) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
have rw₂ : (↑y⁻¹ : M) * a = (↑y⁻¹ : M) * a
Tactic: rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a : M) x y
⊢ (↑a⁻¹ : M) * y = (↑a⁻¹ : M) * (y * (↑a : M) * (↑a⁻¹ : M))
have rw : (↑a⁻¹ : M) * y = (↑a⁻¹ : M) * y
Tactic: rw [Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a : M) x y
⊢ (↑a⁻¹ : M) * (y * (↑a : M) * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
have rw : (↑a⁻¹ : M) * ((↑a : M) * x * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
Tactic: rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a : M) x y
rw : (↑a⁻¹ : M) * ((↑a : M) * x * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
⊢ (↑a⁻¹ : M) * (y * (↑a : M) * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
have rw₁ : (↑a⁻¹ : M) * ((↑a : M) * x) * (↑a⁻¹ : M) = x * (↑a⁻¹ : M)
Tactic: rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a : M) x y
rw : (↑a⁻¹ : M) * ((↑a : M) * x * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
rw₁ : (↑a⁻¹ : M) * ((↑a : M) * x) * (↑a⁻¹ : M) = x * (↑a⁻¹ : M)
⊢ (↑a⁻¹ : M) * (y * (↑a : M) * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
have rw₂ : x * (↑a⁻¹ : M) = x * (↑a⁻¹ : M)
Tactic: rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Units (goal)
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
x : M
⊢ (↑u : M) * x = (↑u : M) * x * (↑u⁻¹ : M) * (↑u : M)
have rw : (↑u : M) * x = (↑u : M) * x
Tactic: rw [Units.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi (f := f) univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
have simp_rw : (↑(pi (f := f) univ H) : Set ((i : η) → f i)) = (↑⊥ : Set ((i : η) → f i)) ↔
  ∀ (i : η), (↑(H i) : Set (f i)) = (↑⊥ : Set (f i))
Tactic: simp_rw [SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
inst_6 : IsMulTorsionFree G
n : ℕ
hn : n ≠ 0
a b : ↥H
⊢ Eq.{u_1 + 1} (α := ↥H) ((fun (a : ↥H) ↦ a ^ n) a) ((fun (a : ↥H) ↦ a ^ n) b) → a = b
have this : Eq.{u_1 + 1} (α := G) ((fun (a : G) ↦ a ^ n) (↑a : G)) ((fun (a : G) ↦ a ^ n) (↑b : G)) → (↑a : G) = (↑b : G)
Tactic: have := pow_left_injective hn (M := G) (a₁ := a) (a₂ := b)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
inst_6 : IsMulTorsionFree G
n : ℕ
hn : ¬n = 0
a b : ↥H
this : (↑a : G) ^ n = (↑b : G) ^ n → (↑a : G) = (↑b : G)
⊢ a ^ n = b ^ n → a = b
have norm_cast : ∀ (this : a ^ n = b ^ n → a = b), a ^ n = b ^ n → a = b
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H
have simp_rw : H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H
Tactic: simp_rw [map_equiv_eq_comap_symm']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H
have simp_rw : H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H
Tactic: simp_rw [map_equiv_eq_comap_symm']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H
have simp_rw : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H
Tactic: simp_rw [map_equiv_eq_comap_symm']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : CommGroup G
s : Set G
⊢ Eq (α := Subgroup G) (normalizer s) ⊤
have h : ∀ (x : G), Membership.mem (γ := Subgroup G) (normalizer s) x ↔ Membership.mem (γ := Subgroup G) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
⊢ Membership.mem (γ := Subgroup G) (normalizer s) g ↔
    (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' s = s
have simp_rw : (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s
Tactic: simp_rw [mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, MulAut.conj_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s
have refine : ∀ (h : G), (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
Tactic: refine forall_congr' fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
have simp_rw : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)
Tactic: simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
have simp_rw₁ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * (h * g)) ↔ h ∈ s)
Tactic: simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)
simp_rw₁ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * (h * g)) ↔ h ∈ s)
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
have simp_rw₂ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * h * g) ↔ h ∈ s)
Tactic: simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)
simp_rw₁ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * (h * g)) ↔ h ∈ s)
simp_rw₂ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * h * g) ↔ h ∈ s)
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
have simp_rw₃ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ (g⁻¹ * h * g ∈ s ↔ h ∈ s)
Tactic: simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer s) g ↔
    (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
              AddAut G) :
          (a : G) → G) ''
        s =
      s
have simp_rw : (∀ (h : G), h ∈ s ↔ -g + h + g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g + x_1 + -g = x) ↔ x ∈ s
Tactic: simp_rw [AddSubgroup.mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, AddAut.conj_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ -g + h + g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g + x_1 + -g = x) ↔ x ∈ s
have refine : ∀ (h : G), (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)
Tactic: refine forall_congr' fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g h : G
⊢ (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)
have simp_rw : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x = h + g) ↔ h ∈ s)
Tactic: simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x = h + g) ↔ h ∈ s)
⊢ (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)
have simp_rw₁ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + (h + g)) ↔ h ∈ s)
Tactic: simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x = h + g) ↔ h ∈ s)
simp_rw₁ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + (h + g)) ↔ h ∈ s)
⊢ (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)
have simp_rw₂ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + h + g) ↔ h ∈ s)
Tactic: simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x = h + g) ↔ h ∈ s)
simp_rw₁ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + (h + g)) ↔ h ∈ s)
simp_rw₂ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + h + g) ↔ h ∈ s)
⊢ (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)
have simp_rw₃ : (h ∈ s ↔ -g + h + g ∈ s) ↔ (-g + h + g ∈ s ↔ h ∈ s)
Tactic: simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (normalizer s) g
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) g
have this : (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
  (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' s)) : Set G)
Tactic: have : MulAut.conj g '' (closure s) = closure (MulAut.conj g '' s) :=
    congr($(MulAut.conj g |>.toMonoidHom.map_closure s))
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (normalizer s) g
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) g
have this₁ : (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: rw [mem_normalizer_iff_conj_image_eq.mp hg] at this
Cleared hypotheses: this