awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((f : (a : R) → S) 1 : S) b = b
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := S) 1 b = b
have rw₁ : HSMul.hSMul.{u_4, u_6, u_6} (α := R) 1 b = b
Tactic: rw [← f.map_one, hsmul, one_smul]
-- 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
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
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := S) 1 b = b
have rw₂ : b = b
Tactic: rw [← f.map_one, hsmul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Hom (goal)
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
have refine : ∀ (x y : G), ∃ (g : E), g • x = y
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Hom (goal)
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_1 : MulAction E G := compHom G f
x y : G
⊢ ∃ (g : E), g • x = y
have obtain : ∀ (m : F), ∃ (g : E), g • x = m • x
Tactic: obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Hom (goal)
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_1 : MulAction E G := compHom G f
x : G
m : F
⊢ ∃ (g : E), g • x = m • x
have obtain : ∀ (e : E), ∃ (g : E), g • x = HSMul.hSMul.{u_5, u_6, u_6} (α := F) ((f : (a : E) → F) e : F) x
Tactic: obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Hom (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : MulOneClass N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
x y : M
⊢ HSMul.hSMul (β := N) (x * y) 1 = HSMul.hSMul (β := N) x 1 * HSMul.hSMul (β := N) y 1
have rw : HSMul.hSMul (β := N) (x * y) 1 = x • HSMul.hSMul (β := N) y 1
Tactic: rw [smul_one_mul, smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Hom (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : MulOneClass N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
x y : M
rw : HSMul.hSMul (β := N) (x * y) 1 = x • HSMul.hSMul (β := N) y 1
⊢ HSMul.hSMul (β := N) (x * y) 1 = HSMul.hSMul (β := N) x 1 * HSMul.hSMul (β := N) y 1
have rw₁ : HSMul.hSMul (β := N) (x * y) 1 = HSMul.hSMul (β := N) (x * y) 1
Tactic: rw [smul_one_mul, smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Opposite (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst : Mul N
inst_1 : SMul M N
inst_2 : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
⊢ x • y • z = y • x • z
have h : ∀ (X : N), x • op X • z = op X • x • z
Tactic: induction y using MulOpposite.rec'
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b_1 : α
x_1 : Option α
inst_2 : SMul M N
inst_3 : IsScalarTower M N α
a : M
b : N
x : Option α
⊢ (a • b) • x = a • b • x
have none : HSMul.hSMul (β := Option α) (a • b) none = a • HSMul.hSMul (β := Option α) b none
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b_1 : α
x_1 : Option α
inst_2 : SMul M N
inst_3 : IsScalarTower M N α
a : M
b : N
x : Option α
none : HSMul.hSMul (β := Option α) (a • b) Option.none = a • HSMul.hSMul (β := Option α) b Option.none
⊢ (a • b) • x = a • b • x
have some : ∀ (val : α), (a • b) • some val = a • b • some val
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b : α
x_1 : Option α
inst_2 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_3 : IsCentralScalar M α
a : M
x : Option α
⊢ MulOpposite.op a • x = a • x
have none : HSMul.hSMul (β := Option α) (MulOpposite.op a) none = HSMul.hSMul (β := Option α) a none
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b : α
x_1 : Option α
inst_2 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_3 : IsCentralScalar M α
a : M
x : Option α
none : HSMul.hSMul (β := Option α) (MulOpposite.op a) Option.none = HSMul.hSMul (β := Option α) a Option.none
⊢ MulOpposite.op a • x = a • x
have some : ∀ (val : α), MulOpposite.op a • some val = a • some val
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
b : Option α
⊢ (a₁ * a₂) • b = a₁ • a₂ • b
have none : HSMul.hSMul (β := Option α) (a₁ * a₂) none = a₁ • HSMul.hSMul (β := Option α) a₂ none
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
b : Option α
none : HSMul.hSMul (β := Option α) (a₁ * a₂) Option.none = a₁ • HSMul.hSMul (β := Option α) a₂ Option.none
⊢ (a₁ * a₂) • b = a₁ • a₂ • b
have some : ∀ (val : α), (a₁ * a₂) • some val = a₁ • a₂ • some val
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
b : Option α
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 b = b
have none : HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Option α) 1 none = none
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Option (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
b : Option α
none : HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Option α) 1 Option.none = Option.none
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 b = b
have some : ∀ (val : α), HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (some val) = some val
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pi (goal)
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
⊢ extend f (r • g) (r • e) = r • extend f g e
have h : ∀ (x : α), extend f (r • g) (r • e) x = (r • extend f g e) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pi (goal)
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x
have h : (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) sorry) else r • e x) =
  HSMul.hSMul (β := β) r
    (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)
Tactic: simp only [extend_def, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pi (goal)
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) else r • e x) =
    HSMul.hSMul (β := β) r
      (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)
have pos : ∀ (h : ∃ (a : ι), f a = x),
  r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) sorry) =
    r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pi (goal)
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
pos :
  ∀ (h : ∃ (a : ι), f a = x),
    r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) =
      r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h)
⊢ (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) else r • e x) =
    HSMul.hSMul (β := β) r
      (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)
have neg : (¬∃ (a : ι), f a = x) → r • e x = r • e x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pi (goal)
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x
have h : (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) sorry) else r • e x) =
  HSMul.hSMul (β := β) r
    (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)
Tactic: classical
  simp only [extend_def, Pi.smul_apply]
  split_ifs <;> rfl
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
⊢ (↑(s • t • u) : Set γ) = (↑(t • s • u) : Set γ)
have simp_rw : (↑s : Set α) • (↑t : Set β) • (↑u : Set γ) = (↑t : Set β) • (↑s : Set α) • (↑u : Set γ)
Tactic: simp_rw [coe_smul, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : DecidableEq β
inst_2 : DecidableEq α
inst_3 : Monoid α
inst_4 : MulAction α β
s : Finset β
⊢ image (fun (b : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 b) s = s
have simp_rw : image (fun (b : β) ↦ b) s = s
Tactic: simp_rw [one_smul, image_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
inst_1 : IsLeftCancelSMul α β
inst_2 : DecidableEq β
s : Set α
t : Finset β
⊢ (Set.PairwiseDisjoint.{u_3, u_2} (α := Finset β) s fun (x : α) ↦ x • t) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
have simp_rw : (Set.PairwiseDisjoint.{u_3, u_2} (α := Set β) s fun (i : α) ↦ (↑(i • t) : Set β)) ↔
  Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
Tactic: simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
inst_1 : IsLeftCancelSMul α β
inst_2 : DecidableEq β
s : Set α
t : Finset β
simp_rw :
  (Set.PairwiseDisjoint.{u_3, u_2} (α := Set β) s fun (i : α) ↦ (↑(i • t) : Set β)) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
⊢ (Set.PairwiseDisjoint.{u_3, u_2} (α := Finset β) s fun (x : α) ↦ x • t) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
have simp_rw₁ : (Set.PairwiseDisjoint.{u_3, u_2} (α := Set β) s fun (i : α) ↦ i • (↑t : Set β)) ↔
  Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
Tactic: simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s
have rw : a • a⁻¹ • b ∈ a • s ↔ b ∈ a • s
Tactic: rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
rw : a • a⁻¹ • b ∈ a • s ↔ b ∈ a • s
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s
have rw₁ : b ∈ a • s ↔ b ∈ a • s
Tactic: rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s
have rw : a • b ∈ a • a⁻¹ • s ↔ a • b ∈ s
Tactic: rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
rw : a • b ∈ a • a⁻¹ • s ↔ a • b ∈ s
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s
have rw₁ : a • b ∈ s ↔ a • b ∈ s
Tactic: rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ (↑(a • s) : Set β) ⊆ (↑t : Set β) ↔ (↑s : Set β) ⊆ (↑(a⁻¹ • t) : Set β)
have push_cast : a • (↑s : Set β) ⊆ (↑t : Set β) ↔ (↑s : Set β) ⊆ a⁻¹ • (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ (↑s : Set β) ⊆ (↑(a • t) : Set β) ↔ (↑(a⁻¹ • s) : Set β) ⊆ (↑t : Set β)
have push_cast : (↑s : Set β) ⊆ a • (↑t : Set β) ↔ a⁻¹ • (↑s : Set β) ⊆ (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
inst_3 : Fintype β
⊢ a • s = univ ↔ s = univ
have rw : s = HSMul.hSMul (β := Finset β) a⁻¹ univ ↔ s = univ
Tactic: rw [smul_eq_iff_eq_inv_smul, smul_finset_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
inst_3 : Fintype β
rw : s = HSMul.hSMul (β := Finset β) a⁻¹ univ ↔ s = univ
⊢ a • s = univ ↔ s = univ
have rw₁ : s = univ ↔ s = univ
Tactic: rw [smul_eq_iff_eq_inv_smul, smul_finset_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nonempty
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)
have push_cast : HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a : α
s : Finset α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹
have h : ∀ (a_1 : α), a_1 ∈ (a • s)⁻¹ ↔ a_1 ∈ op a⁻¹ • s⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Finset (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a : α
s : Finset α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹
have h : ∀ (a_1 : α), a_1 ∈ (op a • s)⁻¹ ↔ a_1 ∈ a⁻¹ • s⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst : Monoid M
inst_1 : (i : ι) → MulAction.{u_5, u_7} M (α i)
c : M
hc : IsUnit c
I : Set ι
s : (i : ι) → Set (α i)
⊢ c • I.pi (α := α) s = I.pi (α := α) (c • s)
have lift : ∀ (c : Mˣ), (↑c : M) • I.pi (α := α) s = I.pi (α := α) ((↑c : M) • s)
Tactic: lift c to Mˣ using hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ op '' s • t = t * s
have rw : Eq (α := Set α) (image2 (fun (a b : α) ↦ op b • a) t s) (image2 (fun (x1 x2 : α) ↦ x1 * x2) t s)
Tactic: rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
a b : α
s : Set α
⊢ {a, b} * s = a • s ∪ b • s
have rw : (fun (x : α) ↦ a * x) '' s ∪ (fun (x : α) ↦ b * x) '' s = a • s ∪ b • s
Tactic: rw [insert_eq, union_mul, singleton_mul, singleton_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
s : Set α
a b : α
⊢ s * {a, b} = s <• a ∪ s <• b
have rw : (fun (x : α) ↦ x * a) '' s ∪ (fun (x : α) ↦ x * b) '' s = s <• a ∪ s <• b
Tactic: rw [insert_eq, mul_union, mul_singleton, mul_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
inst_1 : MulAction α β
s : Set β
⊢ (fun (x2 : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 x2) '' s = s
have simp_rw : (fun (a : β) ↦ a) '' s = s
Tactic: simp_rw [one_smul, image_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B
have refine : A ⊆ (fun (x : β) ↦ a • x) ⁻¹' B ↔ A ⊆ a⁻¹ • B
Tactic: refine image_subset_iff.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun (x : β) ↦ a • x) ⁻¹' B ↔ A ⊆ a⁻¹ • B
have a₁ : (fun (x : β) ↦ a • x) ⁻¹' B = a⁻¹ • B
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ A ⊆ a • B ↔ a⁻¹ • A ⊆ B
have refine : A ⊆ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B
Tactic: refine (image_subset_iff.trans ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B
have a₁ : (fun (x : β) ↦ a⁻¹ • x) ⁻¹' B = a • B
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
⊢ a • s = univ ↔ s = univ
have rw : s = HSMul.hSMul (β := Set β) a⁻¹ univ ↔ s = univ
Tactic: rw [smul_eq_iff_eq_inv_smul, smul_set_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
rw : s = HSMul.hSMul (β := Set β) a⁻¹ univ ↔ s = univ
⊢ a • s = univ ↔ s = univ
have rw₁ : s = univ ↔ s = univ
Tactic: rw [smul_eq_iff_eq_inv_smul, smul_set_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
⊢ a • sᶜ = (a • s)ᶜ
have simp_rw : a • (univ \ s) = univ \ a • s
Tactic: simp_rw [Set.compl_eq_univ_diff, smul_set_sdiff, smul_set_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
a : α
simp_rw : a • (univ \ s) = univ \ a • s
⊢ a • sᶜ = (a • s)ᶜ
have simp_rw₁ : HSMul.hSMul (β := Set β) a univ \ a • s = univ \ a • s
Tactic: simp_rw [Set.compl_eq_univ_diff, smul_set_sdiff, smul_set_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
have mp : (x • s ∩ t).Nonempty → ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
mp : (x • s ∩ t).Nonempty → ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
have mpr : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
have mp : ∀ (b : α) (hb : b ∈ s) (h : x • b ∈ x • s) (ha : x • b ∈ t), ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Tactic: obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
have rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Tactic: rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
have rw₁ : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Tactic: rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
have simp_rw : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
Tactic: simp_rw [smul_inter_nonempty_iff, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
have rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
Tactic: rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff']
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : α
rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
have rw₁ : (∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x) ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
Tactic: rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff']
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
have mp : (x • s ∩ t).Nonempty → ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
mp : (x • s ∩ t).Nonempty → ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
⊢ (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
have mpr : (∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty
Tactic: constructor