awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have pos : ∀ (h : x ∈ s), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
pos : ∀ (h : x ∈ s), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have neg : ∀ (h : ¬x ∈ s), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have pos : (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
Tactic: rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
pos : (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have pos₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = f x
Tactic: rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
pos : (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
pos₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = f x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have pos₂ : f x * sᶜ.mulIndicator g x = f x
Tactic: rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
pos : (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
pos₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = f x
pos₂ : f x * sᶜ.mulIndicator g x = f x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have pos₃ : f x * 1 = f x
Tactic: rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
pos : (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
pos₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = f x
pos₂ : f x * sᶜ.mulIndicator g x = f x
pos₃ : f x * 1 = f x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have pos₄ : f x = f x
Tactic: rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have neg : (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
Tactic: rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
neg : (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have neg₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = g x
Tactic: rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
neg : (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
neg₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have neg₂ : 1 * sᶜ.mulIndicator g x = g x
Tactic: rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
neg : (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
neg₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = g x
neg₂ : 1 * sᶜ.mulIndicator g x = g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have neg₃ : 1 * g x = g x
Tactic: rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
neg : (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
neg₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = g x
neg₂ : 1 * sᶜ.mulIndicator g x = g x
neg₃ : 1 * g x = g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
have neg₄ : g x = g x
Tactic: rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f : α → G
⊢ sᶜ.mulIndicator f = f / s.mulIndicator f
have rw : sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹
Tactic: rw [div_eq_mul_inv, mulIndicator_compl]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f : α → G
rw : sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹
⊢ sᶜ.mulIndicator f = f / s.mulIndicator f
have rw₁ : f * (s.mulIndicator f)⁻¹ = f * (s.mulIndicator f)⁻¹
Tactic: rw [div_eq_mul_inv, mulIndicator_compl]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f * s.mulIndicator f = t.mulIndicator f
have h₁ : Disjoint (t \ s) s
Tactic: rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self,
      union_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
have rw : t.mulIndicator f * (s.mulIndicator f)⁻¹ = t.mulIndicator f / s.mulIndicator f
Tactic: rw [mulIndicator_diff h, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
rw : t.mulIndicator f * (s.mulIndicator f)⁻¹ = t.mulIndicator f / s.mulIndicator f
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
have rw₁ : t.mulIndicator f * (s.mulIndicator f)⁻¹ = t.mulIndicator f * (s.mulIndicator f)⁻¹
Tactic: rw [mulIndicator_diff h, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
have pos : ∀ (hs : x ∈ s), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Tactic: by_cases hs : x ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
pos : ∀ (hs : x ∈ s), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
have neg : ∀ (hs : ¬x ∈ s), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Tactic: by_cases hs : x ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
have pos : ∀ (ht : x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Tactic: by_cases ht : x ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
pos : ∀ (ht : x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
have neg : ∀ (ht : ¬x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Tactic: by_cases ht : x ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
have pos : ∀ (ht : x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Tactic: by_cases ht : x ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
pos : ∀ (ht : x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
have neg : ∀ (ht : ¬x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Tactic: by_cases ht : x ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
⊢ Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}
have by_contra : ∀ (this : ¬Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
⊢ Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}
have suffices : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
Tactic: suffices ∀ j', j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False by by_contra; aesop
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj_1 : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
⊢ False
have hs₁ : ∀ ⦃i j : γ⦄, i ≠ j → ∀ ⦃x : Set α⦄, x ⊆ s i ∧ x ⊆ mulSupport f → x ⊆ s j ∧ x ⊆ mulSupport f → x ⊆ ⊥
Tactic: simp only [Pairwise, Disjoint, Set.le_eq_subset, Set.subset_inter_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
⊢ mulIndicator {i} f = Pi.mulSingle (M := fun (j : ι) ↦ M) i (f i)
have h : ∀ (j : ι), mulIndicator {i} f j = Pi.mulSingle (M := fun (j : ι) ↦ M) i (f i) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
⊢ mulIndicator {i} f j = Pi.mulSingle (M := fun (j : ι) ↦ M) i (f i) j
have h : (if j = i then f j else 1) = if j = i then f i else 1
Tactic: simp only [Set.mulIndicator_apply, Pi.mulSingle_apply, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
⊢ (if j = i then f j else 1) = if j = i then f i else 1
have pos : ∀ (h : j = i), f j = f i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
pos : ∀ (h : j = i), f j = f i
⊢ (if j = i then f j else 1) = if j = i then f i else 1
have neg : ∀ (h : ¬j = i), Eq.{u_7 + 1} (α := M) 1 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
⊢ f (x * y * z) = f (x * (y * z))
have rw : f (x * y) * f z = f (x * (y * z))
Tactic: rw [mul, mul, mul, mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
rw : f (x * y) * f z = f (x * (y * z))
⊢ f (x * y * z) = f (x * (y * z))
have rw₁ : f x * f y * f z = f (x * (y * z))
Tactic: rw [mul, mul, mul, mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
rw : f (x * y) * f z = f (x * (y * z))
rw₁ : f x * f y * f z = f (x * (y * z))
⊢ f (x * y * z) = f (x * (y * z))
have rw₂ : f x * f y * f z = f x * f (y * z)
Tactic: rw [mul, mul, mul, mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
rw : f (x * y) * f z = f (x * (y * z))
rw₁ : f x * f y * f z = f (x * (y * z))
rw₂ : f x * f y * f z = f x * f (y * z)
⊢ f (x * y * z) = f (x * (y * z))
have rw₃ : f x * f y * f z = f x * (f y * f z)
Tactic: rw [mul, mul, mul, mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
rw : f (x * y) * f z = f (x * (y * z))
rw₁ : f x * f y * f z = f (x * (y * z))
rw₂ : f x * f y * f z = f x * f (y * z)
rw₃ : f x * f y * f z = f x * (f y * f z)
⊢ f (x * y * z) = f (x * (y * z))
have rw₄ : f x * (f y * f z) = f x * (f y * f z)
Tactic: rw [mul, mul, mul, mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f (x * y) = f (y * x)
have rw : f x * f y = f (y * x)
Tactic: rw [mul, mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
rw : f x * f y = f (y * x)
⊢ f (x * y) = f (y * x)
have rw₁ : f x * f y = f y * f x
Tactic: rw [mul, mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
rw : f x * f y = f (y * x)
rw₁ : f x * f y = f y * f x
⊢ f (x * y) = f (y * x)
have rw₂ : f y * f x = f y * f x
Tactic: rw [mul, mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f (1 * x) = f x
have rw : f 1 * f x = f x
Tactic: rw [mul, one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f 1 * f x = f x
⊢ f (1 * x) = f x
have rw₁ : 1 * f x = f x
Tactic: rw [mul, one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f 1 * f x = f x
rw₁ : 1 * f x = f x
⊢ f (1 * x) = f x
have rw₂ : f x = f x
Tactic: rw [mul, one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f (x * 1) = f x
have rw : f x * f 1 = f x
Tactic: rw [mul, one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f x * f 1 = f x
⊢ f (x * 1) = f x
have rw₁ : f x * 1 = f x
Tactic: rw [mul, one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f x * f 1 = f x
rw₁ : f x * 1 = f x
⊢ f (x * 1) = f x
have rw₂ : f x = f x
Tactic: rw [mul, one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (HPow.hPow (β := ℕ) x 0) = f 1
have rw : HPow.hPow (β := ℕ) (f x) 0 = f 1
Tactic: rw [npow, one, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
rw : HPow.hPow (β := ℕ) (f x) 0 = f 1
⊢ f (HPow.hPow (β := ℕ) x 0) = f 1
have rw₁ : HPow.hPow (β := ℕ) (f x) 0 = 1
Tactic: rw [npow, one, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
rw : HPow.hPow (β := ℕ) (f x) 0 = f 1
rw₁ : HPow.hPow (β := ℕ) (f x) 0 = 1
⊢ f (HPow.hPow (β := ℕ) x 0) = f 1
have rw₂ : Eq.{u_2 + 1} (α := M₂) 1 1
Tactic: rw [npow, one, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1)) = f (x ^ n * x)
have rw : f x ^ (n + 1) = f (x ^ n * x)
Tactic: rw [npow, pow_succ, mul, npow]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f x ^ (n + 1) = f (x ^ n * x)
⊢ f (x ^ (n + 1)) = f (x ^ n * x)
have rw₁ : f x ^ n * f x = f (x ^ n * x)
Tactic: rw [npow, pow_succ, mul, npow]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f x ^ (n + 1) = f (x ^ n * x)
rw₁ : f x ^ n * f x = f (x ^ n * x)
⊢ f (x ^ (n + 1)) = f (x ^ n * x)
have rw₂ : f x ^ n * f x = f (x ^ n) * f x
Tactic: rw [npow, pow_succ, mul, npow]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f x ^ (n + 1) = f (x ^ n * x)
rw₁ : f x ^ n * f x = f (x ^ n * x)
rw₂ : f x ^ n * f x = f (x ^ n) * f x
⊢ f (x ^ (n + 1)) = f (x ^ n * x)
have rw₃ : f x ^ n * f x = f x ^ n * f x
Tactic: rw [npow, pow_succ, mul, npow]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁_1 : Type u_1
M₂ : Type u_2
inst : Mul M₁_1
inst_1 : One M₁_1
inst_2 : Pow M₁_1 ℕ
M₁ : Type u_3
inst_3 : Inv M₁
inst_4 : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ f x⁻¹⁻¹ = f x
have rw : (f x⁻¹)⁻¹ = f x
Tactic: rw [inv, inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁_1 : Type u_1
M₂ : Type u_2
inst : Mul M₁_1
inst_1 : One M₁_1
inst_2 : Pow M₁_1 ℕ
M₁ : Type u_3
inst_3 : Inv M₁
inst_4 : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
rw : (f x⁻¹)⁻¹ = f x
⊢ f x⁻¹⁻¹ = f x
have rw₁ : (f x)⁻¹⁻¹ = f x
Tactic: rw [inv, inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁_1 : Type u_1
M₂ : Type u_2
inst : Mul M₁_1
inst_1 : One M₁_1
inst_2 : Pow M₁_1 ℕ
M₁ : Type u_3
inst_3 : Inv M₁
inst_4 : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
rw : (f x⁻¹)⁻¹ = f x
rw₁ : (f x)⁻¹⁻¹ = f x
⊢ f x⁻¹⁻¹ = f x
have rw₂ : f x = f x
Tactic: rw [inv, inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ f 1⁻¹ = f 1
have rw : (f 1)⁻¹ = f 1
Tactic: rw [inv, one, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
rw : (f 1)⁻¹ = f 1
⊢ f 1⁻¹ = f 1
have rw₁ : Eq.{u_2 + 1} (α := M₂) 1⁻¹ 1
Tactic: rw [inv, one, inv_one]