awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
inst : Monoid N
inst_1 : SMul M N
H : ∀ (x : M) (y : N), y * HSMul.hSMul (β := N) x 1 = x • y
x : M
y z : N
rw : x • y • z = y • (z * HSMul.hSMul (β := N) x 1)
rw₁ : x • (y * z) = y • (z * HSMul.hSMul (β := N) x 1)
rw₂ : y * z * HSMul.hSMul (β := N) x 1 = y • (z * HSMul.hSMul (β := N) x 1)
rw₃ : y * z * HSMul.hSMul (β := N) x 1 = y * (z * HSMul.hSMul (β := N) x 1)
⊢ x • y • z = y • x • z
have rw₄ : y * (z * HSMul.hSMul (β := N) x 1) = y * (z * HSMul.hSMul (β := N) x 1)
Tactic: rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul N P
inst_4 : SMul N Q
inst_5 : Monoid P
inst_6 : MulAction P Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M P Q
inst_9 : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ (m • n) • q = m • n • q
have rw : HSMul.hSMul (β := P) (m • n) 1 • q = m • n • q
Tactic: rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul N P
inst_4 : SMul N Q
inst_5 : Monoid P
inst_6 : MulAction P Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M P Q
inst_9 : IsScalarTower N P Q
m : M
n : N
q : Q
rw : HSMul.hSMul (β := P) (m • n) 1 • q = m • n • q
⊢ (m • n) • q = m • n • q
have rw₁ : (m • HSMul.hSMul (β := P) n 1) • q = m • n • q
Tactic: rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul N P
inst_4 : SMul N Q
inst_5 : Monoid P
inst_6 : MulAction P Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M P Q
inst_9 : IsScalarTower N P Q
m : M
n : N
q : Q
rw : HSMul.hSMul (β := P) (m • n) 1 • q = m • n • q
rw₁ : (m • HSMul.hSMul (β := P) n 1) • q = m • n • q
⊢ (m • n) • q = m • n • q
have rw₂ : m • HSMul.hSMul (β := P) n 1 • q = m • n • q
Tactic: rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul N P
inst_4 : SMul N Q
inst_5 : Monoid P
inst_6 : MulAction P Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M P Q
inst_9 : IsScalarTower N P Q
m : M
n : N
q : Q
rw : HSMul.hSMul (β := P) (m • n) 1 • q = m • n • q
rw₁ : (m • HSMul.hSMul (β := P) n 1) • q = m • n • q
rw₂ : m • HSMul.hSMul (β := P) n 1 • q = m • n • q
⊢ (m • n) • q = m • n • q
have rw₃ : m • n • q = m • n • q
Tactic: rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ (m • p) • q = m • p • q
have rw : (HSMul.hSMul (β := N) m 1 • p) • q = m • p • q
Tactic: rw [← smul_one_smul N m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower N P Q
m : M
p : P
q : Q
rw : (HSMul.hSMul (β := N) m 1 • p) • q = m • p • q
⊢ (m • p) • q = m • p • q
have rw₁ : HSMul.hSMul (β := N) m 1 • p • q = m • p • q
Tactic: rw [← smul_one_smul N m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower N P Q
m : M
p : P
q : Q
rw : (HSMul.hSMul (β := N) m 1 • p) • q = m • p • q
rw₁ : HSMul.hSMul (β := N) m 1 • p • q = m • p • q
⊢ (m • p) • q = m • p • q
have rw₂ : m • p • q = m • p • q
Tactic: rw [← smul_one_smul N m, smul_assoc, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower M P Q
h : Surjective.{u_9 + 1, u_10 + 1} (β := N) fun (m : M) ↦ HSMul.hSMul (β := N) m 1
n : N
p : P
q : Q
⊢ (n • p) • q = n • p • q
have obtain : ∀ (m : M),
  HSMul.hSMul.{u_10, u_11, u_11} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) p • q =
    HSMul.hSMul.{u_10, u_12, u_12} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) (p • q)
Tactic: obtain ⟨m, rfl⟩ := h n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul P Q
inst_4 : Monoid N
inst_5 : MulAction N P
inst_6 : MulAction N Q
inst_7 : IsScalarTower M N P
inst_8 : IsScalarTower M N Q
inst_9 : IsScalarTower M P Q
h : Surjective.{u_9 + 1, u_10 + 1} (β := N) fun (m : M) ↦ HSMul.hSMul (β := N) m 1
p : P
q : Q
m : M
simp_rw simp_rw₁ : (HSMul.hSMul (β := N) m 1 • p) • q = HSMul.hSMul (β := N) m 1 • p • q
⊢ HSMul.hSMul.{u_10, u_11, u_11} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) p • q =
    HSMul.hSMul.{u_10, u_12, u_12} (α := N) ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) m) (p • q)
have simp_rw₂ : (m • p) • q = m • p • q
Tactic: simp_rw [smul_one_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst : Group G
inst_1 : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ b = c
have rw : a⁻¹ • a • b = c
Tactic: rw [← inv_smul_smul a b, h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst : Group G
inst_1 : MulAction G P
a : G
b c : P
h : a • b = a • c
rw : a⁻¹ • a • b = c
⊢ b = c
have rw₁ : a⁻¹ • a • c = c
Tactic: rw [← inv_smul_smul a b, h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
G_1 : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst : Group G
inst_1 : MulAction G P
a : G
b c : P
h : a • b = a • c
rw : a⁻¹ • a • b = c
rw₁ : a⁻¹ • a • c = c
⊢ b = c
have rw₂ : c = c
Tactic: rw [← inv_smul_smul a b, h, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.End (goal)
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ MulAction.IsPretransitive (Perm α) α
have rw : ∀ (x y : α), ∃ (g : Perm α), g • x = y
Tactic: rw [MulAction.isPretransitive_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.End (goal)
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x y : α
⊢ ∃ (g : Perm α), g • x = y
have h : swap x y • x = y
Tactic: use Equiv.swap x y
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.End (goal)
Goal:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
intro intro₁ : ∀ (x y : α), ∃ (g : Perm α), g • x = y
⊢ ∀ (x y : α), ∃ (g : Perm α), g • x = y
have h : ∀ (x y : α), swap x y • x = y
Tactic: classical
  intro x y
  use Equiv.swap x y
  simp
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f' a = g • a
have rw : ∃ g ∈ S, f a = g • a
Tactic: rw [← hf' ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
A : Set X
hA : A ⊆ f.source
⊢ (f.restr A).source = A
have rw : f.source ∩ A = A
Tactic: rw [restr_source, inter_eq_self_of_subset_right hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
A : Set X
hA : A ⊆ f.source
rw : f.source ∩ A = A
⊢ (f.restr A).source = A
have rw₁ : A = A
Tactic: rw [restr_source, inter_eq_self_of_subset_right hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.restr A = f
have a : (f.restr A).toPartialEquiv = f.toPartialEquiv
Tactic: apply toPartialEquiv_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ (f.restr A).toPartialEquiv = f.toPartialEquiv
have a : f.restr A = f.toPartialEquiv
Tactic: rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
a : f.restr A = f.toPartialEquiv
⊢ (f.restr A).toPartialEquiv = f.toPartialEquiv
have a₁ : f.toPartialEquiv = f.toPartialEquiv
Tactic: rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a : X
⊢ a ∈ A ∩ f ⁻¹' B → ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
have this : ∀ (aA : a ∈ A) (aB : a ∈ f ⁻¹' B), ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
Tactic: ⟨aA, aB⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a : X
aA : a ∈ A
aB : a ∈ f ⁻¹' B
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
have rcases : ∀ (γ : G) (γ_mem : γ ∈ S) (hγ : f a = γ • a), ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
Tactic: rcases hf _ aA with ⟨γ, γ_mem, hγ⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a : X
aA : a ∈ A
aB : a ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
have rcases : ∀ (δ : G) (δ_mem : δ ∈ T) (hδ : g (f a) = δ • f a), ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
Tactic: rcases hg _ aB with ⟨δ, δ_mem, hδ⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a : X
aA : a ∈ A
aB : a ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
δ : G
δ_mem : δ ∈ T
hδ : g (f a) = δ • f a
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
have right : (g ∘ f) a = (δ * γ) • a
Tactic: use δ * γ, Finset.mul_mem_mul δ_mem γ_mem
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a : X
aA : a ∈ A
aB : a ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
δ : G
δ_mem : δ ∈ T
hδ : g (f a) = δ • f a
⊢ (g ∘ f) a = (δ * γ) • a
have right : (g ∘ f) a = δ • γ • a
Tactic: rwa [mul_smul, ← hγ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a : X
aA : a ∈ A
aB : a ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
δ : G
δ_mem : δ ∈ T
hδ : g (f a) = δ • f a
right : (g ∘ f) a = δ • γ • a
⊢ (g ∘ f) a = (δ * γ) • a
have right₁ : (g ∘ f) a = δ • f a
Tactic: rwa [mul_smul, ← hγ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) A (T * S)
have rw : IsDecompOn (g ∘ f) (A ∩ fun (a : X) ↦ B (f a)) (T * S)
Tactic: rw [left_eq_inter.mpr h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a
have rcases : ∀ (γ : G) (γ_mem : γ ∈ S) (hγ : f a = γ • a), ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a
Tactic: rcases hf a ha with ⟨γ, γ_mem, hγ⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a
have right : g (f a) = γ⁻¹ • f a
Tactic: use γ⁻¹, Finset.inv_mem_inv γ_mem
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ g (f a) = γ⁻¹ • f a
have right : g (γ • a) = γ⁻¹ • γ • a
Tactic: rw [hγ, inv_smul_smul, ← hγ, h ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
right : g (γ • a) = γ⁻¹ • γ • a
⊢ g (f a) = γ⁻¹ • f a
have right₁ : g (γ • a) = a
Tactic: rw [hγ, inv_smul_smul, ← hγ, h ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
right : g (γ • a) = γ⁻¹ • γ • a
right₁ : g (γ • a) = a
⊢ g (f a) = γ⁻¹ • f a
have right₂ : g (f a) = a
Tactic: rw [hγ, inv_smul_smul, ← hγ, h ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
right : g (γ • a) = γ⁻¹ • γ • a
right₁ : g (γ • a) = a
right₂ : g (f a) = a
⊢ g (f a) = γ⁻¹ • f a
have right₃ : a = a
Tactic: rw [hγ, inv_smul_smul, ← hγ, h ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
⊢ IsDecompOn (↑f.symm : X → X) f.symm.source f.witness⁻¹
have h : f.symm.source = (↑f.toPartialEquiv : X → X) '' f.source
Tactic: convert! f.isDecompOn.of_leftInvOn f.leftInvOn
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
⊢ f.symm.source = (↑f.toPartialEquiv : X → X) '' f.source
have h : f.symm.source = f.target
Tactic: rw [image_source_eq_target, symm_source]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Equidecomp (goal)
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
h : f.symm.source = f.target
⊢ f.symm.source = (↑f.toPartialEquiv : X → X) '' f.source
have h₁ : f.target = f.target
Tactic: rw [image_source_eq_target, symm_source]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
⊢ FaithfulSMul R A ↔ Injective.{u_4 + 1, u_5 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1
have refine_1 : FaithfulSMul R A →
  ∀ {r₁ r₂ : R}
    (hr :
      Eq.{u_5 + 1} (α := A) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r₁) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r₂))
    (h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂) (a : A), r₁ • a = r₂ • a
Tactic: refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
refine_1 :
  FaithfulSMul R A →
    ∀ {r₁ r₂ : R}
      (hr :
        Eq.{u_5 + 1} (α := A) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r₁)
          ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r₂))
      (h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂) (a : A), r₁ • a = r₂ • a
⊢ FaithfulSMul R A ↔ Injective.{u_4 + 1, u_5 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1
have refine_2 : ∀ (h : Injective.{u_4 + 1, u_5 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1) {r₁ r₂ : R}
  (hr : ∀ (a : A), r₁ • a = r₂ • a),
  Eq.{u_5 + 1} (α := A) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r₁) ((fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r₂)
Tactic: refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
h_1 : FaithfulSMul R A
r₁ r₂ : R
hr : HSMul.hSMul (β := A) r₁ 1 = HSMul.hSMul (β := A) r₂ 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a
have refine_1 : r₁ • (1 * a) = r₂ • (1 * a)
Tactic: rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
h_1 : FaithfulSMul R A
r₁ r₂ : R
hr : HSMul.hSMul (β := A) r₁ 1 = HSMul.hSMul (β := A) r₂ 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
refine_1 : r₁ • (1 * a) = r₂ • (1 * a)
⊢ r₁ • a = r₂ • a
have refine_1₁ : HSMul.hSMul (β := A) r₁ 1 * a = r₂ • (1 * a)
Tactic: rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
h_1 : FaithfulSMul R A
r₁ r₂ : R
hr : HSMul.hSMul (β := A) r₁ 1 = HSMul.hSMul (β := A) r₂ 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
refine_1 : r₁ • (1 * a) = r₂ • (1 * a)
refine_1₁ : HSMul.hSMul (β := A) r₁ 1 * a = r₂ • (1 * a)
⊢ r₁ • a = r₂ • a
have refine_1₂ : HSMul.hSMul (β := A) r₁ 1 * a = HSMul.hSMul (β := A) r₂ 1 * a
Tactic: rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
h_1 : FaithfulSMul R A
r₁ r₂ : R
hr : HSMul.hSMul (β := A) r₁ 1 = HSMul.hSMul (β := A) r₂ 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
refine_1 : r₁ • (1 * a) = r₂ • (1 * a)
refine_1₁ : HSMul.hSMul (β := A) r₁ 1 * a = r₂ • (1 * a)
refine_1₂ : HSMul.hSMul (β := A) r₁ 1 * a = HSMul.hSMul (β := A) r₂ 1 * a
⊢ r₁ • a = r₂ • a
have refine_1₃ : HSMul.hSMul (β := A) r₂ 1 * a = HSMul.hSMul (β := A) r₂ 1 * a
Tactic: rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
have refine_1 : ∀ (h : FaithfulSMul G α) (a : G) (ha : ∀ (a_1 : α), a • a_1 = a_1) (a_1 : α),
  a • a_1 = HSMul.hSMul.{u_2, u_3, u_3} (α := G) 1 a_1
Tactic: refine ⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
refine_1 :
  ∀ (h : FaithfulSMul G α) (a : G) (ha : ∀ (a_1 : α), a • a_1 = a_1) (a_1 : α),
    a • a_1 = HSMul.hSMul.{u_2, u_3, u_3} (α := G) 1 a_1
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
have refine_2 : ∀ (h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1) {a₁ a₂ : G} (h' : ∀ (a : α), a₁ • a = a₂ • a), a₁ = a₂
Tactic: refine ⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂
have rw : ∀ (a : α), (a₂⁻¹ * a₁) • a = a
Tactic: rw [← inv_inv a₂, eq_inv_of_mul_eq_one_left (h (a₂⁻¹ * a₁) ?_), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
inst : Monoid S
inst_1 : MulOneClass T
inst_2 : SMul R S
inst_3 : SMul R T
inst_4 : MulAction S T
inst_5 : IsScalarTower R S S
inst_6 : IsScalarTower R T T
inst_7 : IsScalarTower R S T
inst_8 : FaithfulSMul R T
⊢ FaithfulSMul R S
have rw : Injective.{u_4 + 1, u_5 + 1} (β := S) fun (r : R) ↦ HSMul.hSMul (β := S) r 1
Tactic: rw [faithfulSMul_iff_injective_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
inst : Monoid S
inst_1 : MulOneClass T
inst_2 : SMul R S
inst_3 : SMul R T
inst_4 : MulAction S T
inst_5 : IsScalarTower R S S
inst_6 : IsScalarTower R T T
inst_7 : IsScalarTower R S T
inst_8 : FaithfulSMul R T
⊢ Injective.{u_4 + 1, u_5 + 1} (β := S) fun (r : R) ↦ HSMul.hSMul (β := S) r 1
have refine : Injective.{u_4 + 1, u_6 + 1} (α := R) (β := T)
  ((fun (x : S) ↦ HSMul.hSMul (β := T) x 1) ∘ fun (r : R) ↦ HSMul.hSMul (β := S) r 1)
Tactic: refine .of_comp (f := (· • (1 : T))) ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Faithful (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst : SMul M N
inst_1 : SMul M P
inst_2 : SMul M Q
inst_3 : SMul N P
inst_4 : SMul N Q
inst_5 : SMul P Q
inst_6 : FaithfulSMul P Q
inst_7 : IsScalarTower M N Q
inst_8 : IsScalarTower M P Q
inst_9 : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p
have simp_rw : Eq.{u_7 + 1} (α := Q → Q) (fun (x2 : Q) ↦ ((m • n) • p) • x2) fun (x2 : Q) ↦ (m • n • p) • x2
Tactic: simp_rw [← (smul_left_injective' (α := Q)).eq_iff, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Hom (goal)
Goal:
M_1 : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M_1
inst_1 : MulAction M_1 α
R : Type u_4
S : Type u_5
M : Type u_6
inst_2 : Monoid R
inst_3 : MulAction R M
inst_4 : Monoid S
inst_5 : SMul S M
f : R →* S
hf : Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hsmul : ∀ (c : R) (x : M), HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((f : (a : R) → S) c : S) x = c • x
b : M
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := S) 1 b = b
have rw : HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((f : (a : R) → S) 1 : S) b = b
Tactic: rw [← f.map_one, hsmul, one_smul]