awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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

Tactic:
exact h a (hA' ha)
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
A : Set X
⊢ (f.restr A).toPartialEquiv = f.restr A

Tactic:
rfl

Premises used: PartialEquiv.restr, PartialEquiv.IsImage.restr, rfl
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
rw₁ rw₂ : A = A
⊢ (f.restr A).source = A

Tactic:
rw [restr_source, inter_eq_self_of_subset_right hA]

Premises used: Set.inter_eq_self_of_subset_right, Equidecomp.restr_source
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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).toPartialEquiv = f.toPartialEquiv
⊢ f.restr A = f

Tactic:
apply toPartialEquiv_injective

Premises used: Equidecomp.toPartialEquiv_injective
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
a₁ a₂ : f.toPartialEquiv = f.toPartialEquiv
⊢ (f.restr A).toPartialEquiv = f.toPartialEquiv

Tactic:
rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]

Premises used: PartialEquiv.restr_eq_of_source_subset, Equidecomp.toPartialEquiv_restr
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : SMul G X
f : Equidecomp X G
⊢ f.restr univ = f

Tactic:
restr_of_source_subset <| subset_univ _

Premises used: Set.subset_univ, Equidecomp.restr_of_source_subset
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Monoid G
inst_1 : MulAction G X
⊢ IsDecompOn (G := G) (↑(PartialEquiv.refl X) : X → X) (PartialEquiv.refl X).source {1}

Tactic:
simp [IsDecompOn]

Premises used: Equidecomp.IsDecompOn
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
this : ∀ (aA : a ∈ A) (aB : a ∈ f ⁻¹' B), ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
⊢ a ∈ A ∩ f ⁻¹' B → ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a

Tactic:
⟨aA, aB⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
rcases : ∀ (γ : G) (γ_mem : γ ∈ S) (hγ : f a = γ • a), ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a

Tactic:
rcases hf _ aA with ⟨γ, γ_mem, hγ⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
rcases : ∀ (δ : G) (δ_mem : δ ∈ T) (hδ : g (f a) = δ • f a), ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a = g_1 • a

Tactic:
rcases hg _ aB with ⟨δ, δ_mem, hδ⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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_1 ∈ T * S, (g ∘ f) a = g_1 • a

Tactic:
use δ * γ, Finset.mul_mem_mul δ_mem γ_mem

Premises used: Finset.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
right₁ right₂ right₃ right₄ : (g ∘ f) a = δ • f a
⊢ (g ∘ f) a = (δ * γ) • a

Tactic:
rwa [mul_smul, ← hγ]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
rw : IsDecompOn (g ∘ f) (A ∩ fun (a : X) ↦ B (f a)) (T * S)
⊢ IsDecompOn (g ∘ f) A (T * S)

Tactic:
rw [left_eq_inter.mpr h]

Premises used: Iff.mpr, Set.left_eq_inter
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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 ∩ fun (a : X) ↦ B (f a)) (T * S)

Tactic:
hg.comp' hf

Premises used: Set.Mem, setOf, Set.preimage, Equidecomp.IsDecompOn.comp'
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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 ∩ fun (a : X) ↦ B (f a)) (T * S)

Tactic:
exact hg.comp' hf

Premises used: Equidecomp.IsDecompOn.comp'
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Monoid G
inst_1 : MulAction G X
f g : Equidecomp X G
⊢ ∃ (S : Finset G), IsDecompOn (↑(f.trans g.toPartialEquiv) : X → X) (f.trans g.toPartialEquiv).source S

Tactic:
⟨g.witness * f.witness, g.isDecompOn.comp' f.isDecompOn⟩

Premises used: HMul.hMul, Equidecomp.isDecompOn, Exists.intro, Equidecomp.witness, Equidecomp.IsDecompOn.comp'
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Monoid G
inst_1 : MulAction G X
f g : Equidecomp X G
⊢ ∃ (S : Finset G), IsDecompOn (↑(f.trans g.toPartialEquiv) : X → X) (f.trans g.toPartialEquiv).source S

Tactic:
exact ⟨g.witness * f.witness, g.isDecompOn.comp' f.isDecompOn⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
A B C : Set X
inst : Monoid G
inst_1 : MulAction G X
f g : Equidecomp X G
⊢ ∃ (S : Finset G), IsDecompOn (↑(f.trans g.toPartialEquiv) : X → X) (f.trans g.toPartialEquiv).source S

Tactic:
classical exact ⟨g.witness * f.witness, g.isDecompOn.comp' f.isDecompOn⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
rcases : ∀ (γ : G) (γ_mem : γ ∈ S) (hγ : f a = γ • a), ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a

Tactic:
rcases hf a ha with ⟨γ, γ_mem, hγ⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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 (f a) = γ⁻¹ • f a
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a

Tactic:
use γ⁻¹, Finset.inv_mem_inv γ_mem

Premises used: Finset.inv_mem_inv
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
right₃ right₄ : a = a
⊢ g (f a) = γ⁻¹ • f a

Tactic:
rw [hγ, inv_smul_smul, ← hγ, h ha]

Premises used: inv_smul_smul
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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.toPartialEquiv : X → X) '' f.source) f.witness⁻¹

Tactic:
f.isDecompOn.of_leftInvOn f.leftInvOn

Premises used: Equidecomp.IsDecompOn.of_leftInvOn, Equidecomp.toPartialEquiv, Equidecomp.isDecompOn, PartialEquiv.leftInvOn
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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.toPartialEquiv : X → X) '' f.source
⊢ IsDecompOn (↑f.symm : X → X) f.symm.source f.witness⁻¹

Tactic:
convert! f.isDecompOn.of_leftInvOn f.leftInvOn

Premises used: Equidecomp.IsDecompOn.of_leftInvOn, Equidecomp.toPartialEquiv, Equidecomp.isDecompOn, PartialEquiv.leftInvOn
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
h₁ h₂ : f.target = f.target
⊢ f.symm.source = (↑f.toPartialEquiv : X → X) '' f.source

Tactic:
rw [image_source_eq_target, symm_source]

Premises used: PartialEquiv.image_source_eq_target, PartialEquiv.symm_source
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
⊢ ∃ (S : Finset G), IsDecompOn (↑f.symm : X → X) f.symm.source S

Tactic:
exact ⟨f.witness⁻¹, by
    convert! f.isDecompOn.of_leftInvOn f.leftInvOn
    rw [image_source_eq_target, symm_source]⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
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
⊢ ∃ (S : Finset G), IsDecompOn (↑f.symm : X → X) f.symm.source S

Tactic:
classical exact ⟨f.witness⁻¹, by
    convert! f.isDecompOn.of_leftInvOn f.leftInvOn
    rw [image_source_eq_target, symm_source]⟩
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
x : X
h : x ∈ f.target
⊢ (↑f.symm.toPartialEquiv : X → X) x ∈ f.source

Tactic:
f.toPartialEquiv.map_target h

Premises used: PartialEquiv.map_target, Set.Mem, Equidecomp.toPartialEquiv
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
x : X
h : x ∈ f.source
⊢ (↑f.symm : X → X) ((↑f.toPartialEquiv : X → X) x) = x

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
x : X
h : x ∈ f.target
⊢ (↑f.toPartialEquiv : X → X) ((↑f.symm : X → X) x) = x

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
f : Equidecomp X G
⊢ f.symm.symm = f

Tactic:
rfl

Premises used: Equidecomp.symm, PartialEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
⊢ Involutive.{u_1 + 1} (α := Equidecomp X G) symm

Tactic:
symm_symm

Premises used: Function.Involutive, Equidecomp.symm_symm
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := Equidecomp X G) symm

Tactic:
symm_involutive.bijective

Premises used: Equidecomp.symm_involutive, Function.Involutive.bijective
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
⊢ Eq (α := Equidecomp X G) (symm (refl X G)) (refl X G)

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Set.univ, setOf, Equidecomp.symm, PartialEquiv.symm, Equiv.toPartialEquiv, Equidecomp.refl, PartialEquiv.refl, rfl
-- Module: Mathlib.Algebra.Group.Action.Equidecomp
Goal:
X : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G X
A : Set X
⊢ Eq (α := Equidecomp X G) (symm (restr (refl X G) A)) (restr (refl X G) A)

Tactic:
rfl

Premises used: Set.Mem, PartialEquiv.restr, setOf, Equidecomp.symm, PartialEquiv.symm, Equidecomp.restr, Set.preimage, PartialEquiv.IsImage.restr, rfl
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
inst_1 : FaithfulSMul M α
⊢ Injective.{u_1 + 1, u_3 + 1} (β := α → α) fun (x1 : M) (x2 : α) ↦ x1 • x2

Tactic:
fun _ _ h ↦ FaithfulSMul.eq_of_smul_eq_smul (congr_fun h)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, Function.Injective, congr_fun
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst : MulOneClass R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst : MulOneClass R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst : Mul R
inst_1 : IsRightCancelMul R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h r₁
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst : Mul R
inst_1 : IsLeftCancelMul R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h r₁.unop

Premises used: MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
α : Type u_3
inst : RightCancelMonoid α
⊢ FaithfulSMul α α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
α : Type u_3
inst : LeftCancelMonoid α
⊢ FaithfulSMul αᵐᵒᵖ α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Action.Faithful
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

Tactic:
⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩

Premises used: _private.0.faithfulSMul_iff_injective_smul_one.match_1, FaithfulSMul.mk, Iff.intro, Eq
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
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₂)
⊢ FaithfulSMul R A ↔ Injective.{u_4 + 1, u_5 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1

Tactic:
refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
refine_1₃ refine_1₄ : HSMul.hSMul (β := A) r₂ 1 * a = HSMul.hSMul (β := A) r₂ 1 * a
⊢ r₁ • a = r₂ • a

Tactic:
rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]

Premises used: smul_mul_assoc, one_mul
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
R : Type u_4
A : Type u_5
inst : MulOneClass A
inst_1 : SMul R A
inst_2 : IsScalarTower R A A
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:
simpa using hr 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Action.Faithful
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

Tactic:
⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩

Premises used: FaithfulSMul.eq_of_smul_eq_smul, FaithfulSMul.mk, Iff.intro
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
refine_2 : ∀ (h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1) {a₁ a₂ : G} (h' : ∀ (a : α), a₁ • a = a₂ • a), a₁ = a₂
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1

Tactic:
refine ⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Group.Action.Faithful
Goal:
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
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:
simpa only [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
rw : ∀ (a : α), (a₂⁻¹ * a₁) • a = a
⊢ a₁ = a₂

Tactic:
rw [← inv_inv a₂, eq_inv_of_mul_eq_one_left (h (a₂⁻¹ * a₁) ?_), inv_inv]

Premises used: HMul.hMul, eq_inv_of_mul_eq_one_left, Inv.inv, inv_inv
-- Module: Mathlib.Algebra.Group.Action.Faithful
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₂⁻¹ * a₁) • a = a

Tactic:
simpa only [mul_smul, inv_smul_eq_iff] using h'

Premises used: inv_smul_eq_iff, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
rw : Injective.{u_4 + 1, u_5 + 1} (β := S) fun (r : R) ↦ HSMul.hSMul (β := S) r 1
⊢ FaithfulSMul R S

Tactic:
rw [faithfulSMul_iff_injective_smul_one]

Premises used: faithfulSMul_iff_injective_smul_one
-- Module: Mathlib.Algebra.Group.Action.Faithful
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

Tactic:
.of_comp (f := (· • (1 : T))) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
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)
⊢ Injective.{u_4 + 1, u_5 + 1} (β := S) fun (r : R) ↦ HSMul.hSMul (β := S) r 1

Tactic:
refine .of_comp (f := (· • (1 : T))) ?_
-- Module: Mathlib.Algebra.Group.Action.Faithful
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_6 + 1} (α := R) (β := T)
    ((fun (x : S) ↦ HSMul.hSMul (β := T) x 1) ∘ fun (r : R) ↦ HSMul.hSMul (β := S) r 1)

Tactic:
simpa [Function.comp_def, one_smul, ← faithfulSMul_iff_injective_smul_one]

Premises used: one_smul, Function.comp_def, faithfulSMul_iff_injective_smul_one
-- Module: Mathlib.Algebra.Group.Action.Faithful
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 : IsScalarTower R S S
inst_4 : MulAction S T
inst_5 : IsScalarTower S T T
inst_6 : SMul R T
inst_7 : IsScalarTower R T T
inst_8 : IsScalarTower R S T
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S T
⊢ FaithfulSMul R T

Tactic:
simpa [faithfulSMul_iff_injective_smul_one, Function.comp_def] using
    ((faithfulSMul_iff_injective_smul_one S T).mp ‹_›).comp
      ((faithfulSMul_iff_injective_smul_one R S).mp ‹_›)

Premises used: Function.comp_def, Function.Injective.comp, Iff.mp, faithfulSMul_iff_injective_smul_one
-- Module: Mathlib.Algebra.Group.Action.Faithful
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
simp_rw : Eq.{u_7 + 1} (α := Q → Q) (fun (x2 : Q) ↦ ((m • n) • p) • x2) fun (x2 : Q) ↦ (m • n • p) • x2
⊢ (m • n) • p = m • n • p

Tactic:
simp_rw [← (smul_left_injective' (α := Q)).eq_iff, smul_assoc]

Premises used: smul_left_injective', Function.Injective.eq_iff, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Group.Action.Hom
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
a b : R
x : M
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) • x =
    HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((f : (a : R) → S) a : S)
      (HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((f : (a : R) → S) b : S) x)

Tactic:
simp only [← f.map_mul, hsmul, mul_smul]

Premises used: MonoidHom.map_mul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Hom
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
rw : HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((f : (a : R) → S) 1 : S) b = b
rw₁ : HSMul.hSMul.{u_4, u_6, u_6} (α := R) 1 b = b
rw₂ rw₃ : b = b
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := S) 1 b = b

Tactic:
rw [← f.map_one, hsmul, one_smul]

Premises used: one_smul, MonoidHom.map_one
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
g : N →* M
x x_1 : N
x_2 : α
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
simpa [(· • ·)] using mul_smul ..

Premises used: HSMul.hSMul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
g : N →* M
x : α
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := N) 1 x = x

Tactic:
simpa [(· • ·)] using one_smul ..

Premises used: one_smul, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
f : E →* F
a : E
x : G
⊢ a • x = HSMul.hSMul.{u_5, u_6, u_6} (α := F) ((f : (a : E) → F) a : F) x

Tactic:
rfl

Premises used: SMul.comp.smul, rfl
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x : MulAction E G := compHom G f
⊢ IsPretransitive E G

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: MulAction.IsPretransitive.mk