awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Defs (goal)
Goal:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
rw : a = (↑⋯.unit : M) * 1
rw₁ : a = a * 1
⊢ (↑⋯.unit⁻¹ : M) * a = 1
have rw₂ : a = a
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Equiv (goal)
Goal:
G : Type u_6
inst : Group G
x : Gˣ
⊢ (toUnits : (a : G) → Gˣ) (↑x : G) = x
have simp_rw : (↑x : G) = (MulEquiv.symm toUnits : (a : Gˣ) → G) x
Tactic: simp_rw [MulEquiv.apply_eq_iff_symm_apply, toUnits_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Bijective.{u + 1, v + 1} (α := Mˣ) (β := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)
have refine : Surjective.{u + 1, v + 1} (α := Mˣ) (β := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)
Tactic: refine ⟨map_injective hf.injective, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
u v : N
uv : u * v = 1
vu : v * u = 1
⊢ ∃ (a : Mˣ), (map f : (a : Mˣ) → Nˣ) a = { val := u, inv := v, val_inv := uv, inv_val := vu : Nˣ }
have rcases : ∀ (u v : M) (uv : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) u : N) ((f : (a : M) → N) v : N) = 1)
  (vu : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) v : N) ((f : (a : M) → N) u : N) = 1),
  ∃ (a : Mˣ),
    Eq.{v + 1} (α := Nˣ) ((map f : (a : Mˣ) → Nˣ) a : Nˣ)
      ({ val := (f : (a : M) → N) u, inv := (f : (a : M) → N) v, val_inv := uv, inv_val := vu } : Nˣ)
Tactic: rcases hf.surjective u, hf.surjective v with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩
Cleared hypotheses: u, v, uv, vu
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
inst : Monoid M
⊢ Eq (α := Mˣ →* Mˣ) (map (MonoidHom.id M)) (MonoidHom.id Mˣ)
have h : ∀ (x : Mˣ),
  Eq.{u + 1} (α := M) (↑((map (MonoidHom.id M) : (a : Mˣ) → Mˣ) x) : M) (↑((MonoidHom.id Mˣ : (a : Mˣ) → Mˣ) x) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
⊢ g 1 = 1
have huv : (↑(g 1) : N) = (↑1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
⊢ (↑(g 1) : N) = (↑1 : N)
have huv : Eq.{v + 1} (α := N) ((f : (a : M) → N) 1 : N) ((↑1 : N) : N)
Tactic: rw [h 1]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) = 1
have rw : (f : (a : M) → N) x = HMul.hMul (α := N) 1 (↑((liftRight f g h : (a : M) → Nˣ) x) : N)
Tactic: rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
rw : (f : (a : M) → N) x = HMul.hMul (α := N) 1 (↑((liftRight f g h : (a : M) → Nˣ) x) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) = 1
have rw₁ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N)
Tactic: rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
rw : (f : (a : M) → N) x = HMul.hMul (α := N) 1 (↑((liftRight f g h : (a : M) → Nˣ) x) : N)
rw₁ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) = 1
have rw₂ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
⊢ HMul.hMul (α := N) (β := N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) ((f : (a : M) → N) x : N) = 1
have rw : (f : (a : M) → N) x = HMul.hMul (α := N) (↑((liftRight f g h : (a : M) → Nˣ) x) : N) 1
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
rw : (f : (a : M) → N) x = HMul.hMul (α := N) (↑((liftRight f g h : (a : M) → Nˣ) x) : N) 1
⊢ HMul.hMul (α := N) (β := N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) ((f : (a : M) → N) x : N) = 1
have rw₁ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N)
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
rw : (f : (a : M) → N) x = HMul.hMul (α := N) (↑((liftRight f g h : (a : M) → Nˣ) x) : N) 1
rw₁ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N)
⊢ HMul.hMul (α := N) (β := N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) ((f : (a : M) → N) x : N) = 1
have rw₂ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommMonoid M
f g : G →* M
⊢ (f * g).toHomUnits = f.toHomUnits * g.toHomUnits
have h : ∀ (x : G),
  Eq.{u_2 + 1} (α := M) (↑(((f * g).toHomUnits : (a : G) → Mˣ) x) : M)
    (↑((f.toHomUnits * g.toHomUnits : (a : G) → Mˣ) x) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
have rcases : ∀ (y : Mˣ), IsUnit.{u_4} (M := N) ((f : (a : M) → N) (↑y : M) : N)
Tactic: rcases h with ⟨y, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Hom (goal)
Goal:
G : Type u_1
R : Type u_2
S : Type u_3
F : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
inst_4 : FunLike G S R
inst_5 : MonoidHomClass G S R
f : F
g : G
hfg : LeftInverse.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_3} (M := S) ((f : (a : R) → S) a : S)
⊢ IsUnit a
have rwa : ∀ (ha : IsUnit a), IsUnit a
Tactic: rwa [isUnit_map_of_leftInverse g hfg] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : InvolutiveInv α
a : WithOne α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a
have simp_rw : Option.map id a = a
Tactic: simp_rw [inv_comp_inv, Option.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : InvolutiveInv α
a : WithOne α
simp_rw : Option.map id a = a
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a
have simp_rw₁ : id a = a
Tactic: simp_rw [inv_comp_inv, Option.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
inst : Mul α
⊢ Eq (α := WithOne α →* WithOne α) (mapMulHom (MulHom.id α)) (MonoidHom.id (WithOne α))
have h : ∀ (x : WithOne α),
  Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) x : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) x : WithOne α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
inst : Mul α
x : WithOne α
⊢ Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) x : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) x : WithOne α)
have h : Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
  ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
inst : Mul α
x : WithOne α
h :
  Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
⊢ Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) x : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) x : WithOne α)
have h₁ : ∀ (a : α),
  Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) (↑a : WithOne α) : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) (↑a : WithOne α) : WithOne α)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
⊢ Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) x) : WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) x : WithOne γ)
have one : Eq.{w + 1} (α := WithOne γ)
  ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) 1) : WithOne γ)
  ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) 1 : WithOne γ)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
one :
  Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) 1) : WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) 1 : WithOne γ)
⊢ Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) x) : WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) x : WithOne γ)
have coe : ∀ (a : α),
  Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) (↑a : WithOne α)) :
      WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) (↑a : WithOne α) : WithOne γ)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Defs (goal)
Goal:
α : Type u
inst : Semigroup α
a b c : α
⊢ (↑a : WithOne α) * (↑b : WithOne α) * (↑c : WithOne α) = (↑a : WithOne α) * ((↑b : WithOne α) * (↑c : WithOne α))
have simp_rw : (↑(a * b * c) : WithOne α) = (↑(a * (b * c)) : WithOne α)
Tactic: simp_rw [← coe_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
⊢ map₂ f a 1 = 1
have one : map₂ f 1 1 = 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
one : map₂ f 1 1 = 1
⊢ map₂ f a 1 = 1
have coe : ∀ (a : α), map₂ f (↑a : WithOne α) 1 = 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
b : β
⊢ map₂ f a (↑b : WithOne β) = map (fun (x : α) ↦ f x b) a
have one : map₂ f 1 (↑b : WithOne β) = map (fun (x : α) ↦ f x b) 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.WithOne.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
b : β
one : map₂ f 1 (↑b : WithOne β) = map (fun (x : α) ↦ f x b) 1
⊢ map₂ f a (↑b : WithOne β) = map (fun (x : α) ↦ f x b) a
have coe : ∀ (a : α), map₂ f (↑a : WithOne α) (↑b : WithOne β) = map (fun (x : α) ↦ f x b) (↑a : WithOne α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
R : Type u_7
inst : Group G
inst_1 : Monoid R
inst_2 : AddGroup R
inst_3 : DistribMulAction G R
inst_4 : IsScalarTower G R R
inst_5 : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
have rw : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (r • (1 - r⁻¹ • a))
Tactic: rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
R : Type u_7
inst : Group G
inst_1 : Monoid R
inst_2 : AddGroup R
inst_3 : DistribMulAction G R
inst_4 : IsScalarTower G R R
inst_5 : SMulCommClass G R R
r : G
a : R
rw : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (r • (1 - r⁻¹ • a))
⊢ IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
have rw₁ : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (HSMul.hSMul (β := R) r 1 - r • r⁻¹ • a)
Tactic: rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
R : Type u_7
inst : Group G
inst_1 : Monoid R
inst_2 : AddGroup R
inst_3 : DistribMulAction G R
inst_4 : IsScalarTower G R R
inst_5 : SMulCommClass G R R
r : G
a : R
rw : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (r • (1 - r⁻¹ • a))
rw₁ : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (HSMul.hSMul (β := R) r 1 - r • r⁻¹ • a)
⊢ IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
have rw₂ : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (HSMul.hSMul (β := R) r 1 - a)
Tactic: rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (hypothesis)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
⊢ (g / h) • (a / b) = g • a / h • b
have this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
Tactic: have (x : G) : x • (0 : G₀) = 0 := by simpa using (smul_assoc x (0 : G₀) (0 : G₀)).symm
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
⊢ (g / h) • (a / b) = g • a / h • b
have pos : ∀ (hb : b = 0), (g / h) • (a / b) = g • a / h • b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
pos : ∀ (hb : b = 0), (g / h) • (a / b) = g • a / h • b
⊢ (g / h) • (a / b) = g • a / h • b
have neg : ∀ (hb : ¬b = 0), (g / h) • (a / b) = g • a / h • b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
⊢ h • b ≠ 0
have refine : Ne.{u_2 + 1} (α := G₀) ((fun (x : G₀) ↦ h⁻¹ • x) (h • b)) ((fun (x : G₀) ↦ h⁻¹ • x) 0)
Tactic: refine (ne_of_apply_ne (h⁻¹ • ·) ?_)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (hypothesis)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
⊢ (g / h) • (a / b) = g • a / h • b
have this₁ : h • b ≠ 0
Tactic: have : h • b ≠ 0 := by
    refine (ne_of_apply_ne (h⁻¹ • ·) ?_)
    simpa [this]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this_1 : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h) • (a / b) = g • a / h • b
have neg : (g / h * h) • (a / b * b) = g • a
Tactic: rw [eq_div_iff_mul_eq this, smul_mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G G₀
g : G
x : G₀
n : ℤ
⊢ g • x ^ n = (g • x) ^ n
have ofNat : ∀ (a : ℕ), g • x ^ Int.ofNat a = (g • x) ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Basic (goal)
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G G₀
g : G
x : G₀
n : ℤ
ofNat : ∀ (a : ℕ), g • x ^ Int.ofNat a = (g • x) ^ Int.ofNat a
⊢ g • x ^ n = (g • x) ^ n
have negSucc : ∀ (a : ℕ), g • x ^ Int.negSucc a = (g • x) ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Center (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ ↥(Submonoid.center G₀)
have refine : ∀ (r : G₀), r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r
Tactic: refine ⟨(u : G₀ˣ), Submonoid.mem_center_iff.mpr fun r ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Center (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
⊢ r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r
have inl : 0 * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * 0
Tactic: obtain rfl | hr := eq_or_ne r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Center (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
inl : 0 * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * 0
⊢ r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r
have inr : ∀ (hr : r ≠ 0), r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r
Tactic: obtain rfl | hr := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Center (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ 0 * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * 0
have inl : 0 * (↑(↑u : G₀ˣ) : G₀) = 0
Tactic: rw [mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Center (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
inl : 0 * (↑(↑u : G₀ˣ) : G₀) = 0
⊢ 0 * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * 0
have inl₁ : Eq.{u_1 + 1} (α := G₀) 0 0
Tactic: rw [mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.ConjAct (goal)
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : SMul α G₀
inst_2 : SMulCommClass α G₀ G₀
inst_3 : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
⊢ a • ug • g = ug • a • g
have rw : a •
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
  ug • a • g
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.ConjAct (goal)
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : SMul α G₀
inst_2 : SMulCommClass α G₀ G₀
inst_3 : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
rw :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    ug • a • g
⊢ a • ug • g = ug • a • g
have rw₁ : a •
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
  HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) (a • g))
    (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.ConjAct (goal)
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : SMul α G₀
inst_2 : SMulCommClass α G₀ G₀
inst_3 : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
rw :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    ug • a • g
rw₁ :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) (a • g))
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
⊢ a • ug • g = ug • a • g
have rw₂ : a •
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
  HMul.hMul (β := G₀) (a • HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
    (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.ConjAct (goal)
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : SMul α G₀
inst_2 : SMulCommClass α G₀ G₀
inst_3 : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
rw :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    ug • a • g
rw₁ :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) (a • g))
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
rw₂ :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    HMul.hMul (β := G₀) (a • HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
⊢ a • ug • g = ug • a • g
have rw₃ : a •
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
  a •
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
p : Prop
inst_2 : Decidable p
a : M
b : A
⊢ (a • if p then b else 0) = if p then a • b else 0
have pos : p → a • b = a • b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
p : Prop
inst_2 : Decidable p
a : M
b : A
pos : p → a • b = a • b
⊢ (a • if p then b else 0) = if p then a • b else 0
have neg : ¬p → HSMul.hSMul (β := A) a 0 = 0
Tactic: split_ifs