awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
inst : Mul M
N : Type u_5
inst_1 : Mul N
f : M →ₙ* N
⊢ (↑f.srange : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
have rw : Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
  Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
Tactic: rw [coe_srange, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
inst : Mul M
N : Type u_5
inst_1 : Mul N
f : M →ₙ* N
rw :
  Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
⊢ (↑f.srange : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
have rw₁ : Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
  Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
Tactic: rw [coe_srange, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g (⇑f : (a : M) → N)
x : ↥f.srange
x' : M
hx' : (f : (a : M) → N) x' = (↑x : N)
⊢ (f : (a : M) → N) (g (↑x : N)) = (↑x : N)
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (g ((f : (a : M) → N) x')) : N) ((f : (a : M) → N) x' : N)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g (⇑f : (a : M) → N)
x : ↥f.srange
x' : M
hx' : (f : (a : M) → N) x' = (↑x : N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (g ((f : (a : M) → N) x')) : N) ((f : (a : M) → N) x' : N)
⊢ (f : (a : M) → N) (g (↑x : N)) = (↑x : N)
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x' : N) ((f : (a : M) → N) x' : N)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Group.Support (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ n) ⊆ mulSupport f
have zero : (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0) ⊆ mulSupport f
Tactic: induction n with
  | zero => simp [pow_zero]
  | succ n hfn =>
    simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Support (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
f : α → M
n : ℕ
zero : (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0) ⊆ mulSupport f
⊢ (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ n) ⊆ mulSupport f
have succ : ∀ (n : ℕ) (hfn : (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ n) ⊆ mulSupport f),
  (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ (n + 1)) ⊆ mulSupport f
Tactic: induction n with
  | zero => simp [pow_zero]
  | succ n hfn =>
    simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1
have rw : a ^ n = 1 ↔ a ^ n = HPow.hPow (α := M) 1 n
Tactic: rw [← pow_left_inj (a := a) hn, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
rw : a ^ n = 1 ↔ a ^ n = HPow.hPow (α := M) 1 n
⊢ a ^ n = 1 ↔ a = 1
have rw₁ : a ^ n = 1 ↔ a ^ n = 1
Tactic: rw [← pow_left_inj (a := a) hn, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0
have inl : HPow.hPow (β := ℕ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℕ) 0 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
inl : HPow.hPow (β := ℕ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℕ) 0 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0
have inr : ∀ (hn : n ≠ 0), a ^ n = 1 ↔ a = 1 ∨ n = 0
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1
have rw : a ^ n = 1 ↔ a ^ n = HPow.hPow (α := G) 1 n
Tactic: rw [← zpow_left_inj (a := a) hn, one_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
rw : a ^ n = 1 ↔ a ^ n = HPow.hPow (α := G) 1 n
⊢ a ^ n = 1 ↔ a = 1
have rw₁ : a ^ n = 1 ↔ a ^ n = 1
Tactic: rw [← zpow_left_inj (a := a) hn, one_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0
have inl : HPow.hPow (β := ℤ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℤ) 0 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
inl : HPow.hPow (β := ℤ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℤ) 0 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0
have inr : ∀ (hn : n ≠ 0), a ^ n = 1 ↔ a = 1 ∨ n = 0
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
⊢ a = a⁻¹ ↔ a = 1
have rw : a = a⁻¹ ↔ HPow.hPow (β := ℕ) a 2 = 1
Tactic: rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
rw : a = a⁻¹ ↔ HPow.hPow (β := ℕ) a 2 = 1
⊢ a = a⁻¹ ↔ a = 1
have rw₁ : a = a⁻¹ ↔ a * a = 1
Tactic: rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
rw : a = a⁻¹ ↔ HPow.hPow (β := ℕ) a 2 = 1
rw₁ : a = a⁻¹ ↔ a * a = 1
⊢ a = a⁻¹ ↔ a = 1
have rw₂ : a = a⁻¹ ↔ a = a⁻¹
Tactic: rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
⊢ a⁻¹ = a ↔ a = 1
have rw : a = a⁻¹ ↔ a = 1
Tactic: rw [eq_comm, self_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Torsion (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
rw : a = a⁻¹ ↔ a = 1
⊢ a⁻¹ = a ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [eq_comm, self_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Semigroup β
mul : Mul α := e.mul
⊢ Semigroup α
have apply : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.semigroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommSemigroup β
mul : Mul α := e.mul
⊢ CommSemigroup α
have apply : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commSemigroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
⊢ MulOneClass α
have one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.mulOneClass _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ MulOneClass α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.mulOneClass _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ Monoid α
have one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.monoid _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ Monoid α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.monoid _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ Monoid α
have npow : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.monoid _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommMonoid α
have one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.commMonoid _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ CommMonoid α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commMonoid _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ CommMonoid α
have npow : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.commMonoid _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Group α
have one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.group _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ Group α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.group _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ Group α
have inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
Tactic: apply e.injective.group _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
⊢ Group α
have div₁ : ∀ (x y : α), (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.group _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ Group α
have npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.group _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ Group α
have zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.group _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ CommGroup α
have one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.commGroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ CommGroup α
have mul₁ : ∀ (x y : α), (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commGroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ CommGroup α
have inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
Tactic: apply e.injective.commGroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
⊢ CommGroup α
have div₁ : ∀ (x y : α), (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commGroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ CommGroup α
have npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.commGroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ CommGroup α
have zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.commGroup _
-- Lean 4 proof step from Mathlib.Algebra.Group.TransferInstance (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
⊢ ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')
have obtain : ∀ (n : ℕ) (e : G ≃ Fin n), ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
f : G → α
⊢ τ 0 f = f
have h : ∀ (x : G), τ 0 f x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ (a + b) f
have h : ∀ (x : G), τ a (τ b f) x = τ (a + b) f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ a (τ b f)
have h : ∀ (x : G), τ (a + b) f x = τ a (τ b f) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ b (τ a f)
have rw : τ (b + a) f = τ b (τ a f)
Tactic: rw [add_comm, translate_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
rw : τ (b + a) f = τ b (τ a f)
⊢ τ (a + b) f = τ b (τ a f)
have rw₁ : τ b (τ a f) = τ b (τ a f)
Tactic: rw [add_comm, translate_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ b (τ a f)
have rw : τ (a + b) f = τ b (τ a f)
Tactic: rw [← translate_add, translate_add']
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
rw : τ (a + b) f = τ b (τ a f)
⊢ τ a (τ b f) = τ b (τ a f)
have rw₁ : τ b (τ a f) = τ b (τ a f)
Tactic: rw [← translate_add, translate_add']
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a : G
f : G → α
⊢ τ a f = HVAdd.hVAdd (α := Gᵈᵃᵃ) ((DomAddAct.mk : (a : G) → Gᵈᵃᵃ) (-a) : Gᵈᵃᵃ) f
have h : ∀ (x : G), τ a f x = HVAdd.hVAdd (α := Gᵈᵃᵃ) ((DomAddAct.mk : (a : G) → Gᵈᵃᵃ) (-a) : Gᵈᵃᵃ) f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
ι : Type u_1
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ Eq (α := G → M) (τ a (∑ i ∈ s, f i)) (∑ i ∈ s, τ a (f i))
have h : ∀ (x : G), Eq.{u_4 + 1} (α := M) (τ a (∑ i ∈ s, f i) x) ((∑ i ∈ s, τ a (f i)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
G : Type u_5
H : Type u_6
inst : AddCommGroup G
inst_1 : AddCommGroup H
a : G
f : G → H
⊢ support (τ a f) = a +ᵥ support f
have h : ∀ (x : G), x ∈ support (τ a f) ↔ x ∈ a +ᵥ support f
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Translate (goal)
Goal:
ι : Type u_1
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ Eq (α := G → M) (τ a (∏ i ∈ s, f i)) (∏ i ∈ s, τ a (f i))
have h : ∀ (x : G), Eq.{u_4 + 1} (α := M) (τ a (∏ i ∈ s, f i) x) ((∏ i ∈ s, τ a (f i)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
⊢ Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) i
      ((ofAdd : (a : M i) → Multiplicative (M i)) a : Multiplicative (M i)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) i a j))
have inl : ∀ (a : M j),
  Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) j
      ((ofAdd : (a : M j) → Multiplicative (M j)) a : Multiplicative (M j)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) j a j))
Tactic: rcases eq_or_ne j i with rfl | h
Cleared hypotheses: i, a