awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Mul (f i)
x y : (i : I) → f i
⊢ Commute x y ↔ ∀ (i : I), Commute (x i) (y i)

Tactic:
semiconjBy_iff

Premises used: Commute, Pi.semiconjBy_iff
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → One (f i)
inst_1 : DecidableEq I
i : I
⊢ Eq (α := (a : I) → f a) (update (β := f) 1 i 1) 1

Tactic:
update_eq_self i (1 : (a : I) → f a)

Premises used: Function.update_eq_self, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Mul (f i)
inst_1 : DecidableEq I
f₁ f₂ : (i : I) → f i
i : I
x₁ x₂ : f i
⊢ update (β := f) (f₁ * f₂) i (x₁ * x₂) = update (β := f) f₁ i x₁ * update (β := f) f₂ i x₂

Tactic:
funext fun j => (apply_update₂ (fun _ => (· * ·)) f₁ f₂ i x₁ x₂ j).symm

Premises used: HMul.hMul, funext, Function.apply_update₂, Eq.symm
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Inv (f i)
inst_1 : DecidableEq I
f₁ : (i : I) → f i
i : I
x₁ : f i
⊢ update (β := f) f₁⁻¹ i x₁⁻¹ = (update (β := f) f₁ i x₁)⁻¹

Tactic:
funext fun j => (apply_update (fun _ => Inv.inv) f₁ i x₁ j).symm

Premises used: Function.apply_update, funext, Inv.inv, Eq.symm
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Div (f i)
inst_1 : DecidableEq I
f₁ f₂ : (i : I) → f i
i : I
x₁ x₂ : f i
⊢ update (β := f) (f₁ / f₂) i (x₁ / x₂) = update (β := f) f₁ i x₁ / update (β := f) f₂ i x₂

Tactic:
funext fun j => (apply_update₂ (fun _ => (· / ·)) f₁ f₂ i x₁ x₂ j).symm

Premises used: HDiv.hDiv, funext, Function.apply_update₂, Eq.symm
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α : Type u_2
inst : One α
inst_1 : Nonempty ι
a : α
⊢ const ι a = 1 ↔ a = 1

Tactic:
@const_inj _ _ _ _ 1

Premises used: Function.const_inj
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α : Type u_2
inst : One α
inst_1 : Nonempty ι
a : α
⊢ const ι a ≠ 1 ↔ a ≠ 1

Tactic:
Iff.not const_eq_one

Premises used: Function.const_eq_one, Iff.not
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Mul (f i)
s : Set I
inst_1 : (i : I) → Decidable (i ∈ s)
f₁ f₂ g₁ g₂ : (i : I) → f i
⊢ s.piecewise (β := f) (f₁ * f₂) (g₁ * g₂) = s.piecewise (β := f) f₁ g₁ * s.piecewise (β := f) f₂ g₂

Tactic:
s.piecewise_op₂ f₁ _ _ _ fun _ => (· * ·)

Premises used: HMul.hMul, Set.piecewise_op₂
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Inv (f i)
s : Set I
inst_1 : (i : I) → Decidable (i ∈ s)
f₁ g₁ : (i : I) → f i
⊢ s.piecewise (β := f) f₁⁻¹ g₁⁻¹ = (s.piecewise (β := f) f₁ g₁)⁻¹

Tactic:
s.piecewise_op f₁ g₁ fun _ x => x⁻¹

Premises used: Inv.inv, Set.piecewise_op
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Div (f i)
s : Set I
inst_1 : (i : I) → Decidable (i ∈ s)
f₁ f₂ g₁ g₂ : (i : I) → f i
⊢ s.piecewise (β := f) (f₁ / f₂) (g₁ / g₂) = s.piecewise (β := f) f₁ g₁ / s.piecewise (β := f) f₂ g₂

Tactic:
s.piecewise_op₂ f₁ _ _ _ fun _ => (· / ·)

Premises used: Set.piecewise_op₂, HDiv.hDiv
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α : Type u_2
I : Type u
f_1 : I → Type v
M : ι → Type u_3
i : I
η : Type v
R : Type w
s : ι → η
inst : MulOneClass R
f g : ι → R
⊢ extend s (f * g) 1 = extend s f 1 * extend s g 1

Tactic:
simpa using Function.extend_mul s f g 1 1

Premises used: Function.extend_mul, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Preorder (f i)
inst_2 : (i : I) → One (f i)
⊢ Monotone (α := f i) (mulSingle (M := f) i)

Tactic:
Function.update_mono

Premises used: Function.update_mono, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Preorder (f i)
inst_2 : (i : I) → One (f i)
⊢ StrictMono (α := f i) (mulSingle (M := f) i)

Tactic:
Function.update_strictMono

Premises used: Function.update_strictMono, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_2
m : Type u_4
n : Type u_5
inst : DecidableEq n
inst_1 : DecidableEq m
inst_2 : One α
σ : n ≃ m
i : m
x : α
h :
  ∀ (x_1 : n),
    Eq.{u_2 + 1} (α := α) ((mulSingle (M := fun (a : m) ↦ α) i x ∘ (⇑σ : (a : n) → m)) x_1 : α)
      (mulSingle (M := fun (j : n) ↦ α) ((σ.symm : (a : m) → n) i) x x_1 : α)
⊢ Eq (α := n → α) (mulSingle (M := fun (a : m) ↦ α) i x ∘ (⇑σ : (a : n) → m) : n → α)
    (mulSingle (M := fun (j : n) ↦ α) ((σ.symm : (a : m) → n) i) x : (j : n) → α)

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_2
m : Type u_4
n : Type u_5
inst : DecidableEq n
inst_1 : DecidableEq m
inst_2 : One α
σ : n ≃ m
i : m
x_1 : α
x : n
⊢ Eq.{u_2 + 1} (α := α) ((mulSingle (M := fun (a : m) ↦ α) i x_1 ∘ (⇑σ : (a : n) → m)) x : α)
    (mulSingle (M := fun (j : n) ↦ α) ((σ.symm : (a : m) → n) i) x_1 x : α)

Tactic:
aesop (add simp Pi.mulSingle_apply)

Premises used: Pi.mulSingle_apply
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : (a : α) → (b : β a) → One (γ a b)
⊢ Eq (α := (x : α) → (y : β x) → γ x y) (curry (β := fun (a : α) ↦ β a) (γ := γ) 1) 1

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : (a : α) → (b : β a) → One (γ a b)
⊢ Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β))) (uncurry (β := β) (γ := γ) 1) 1

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : (a : α) → (b : β a) → Mul (γ a b)
x y : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ) (x * y) =
    curry (β := fun (a : α) ↦ β a) (γ := γ) x * curry (β := fun (a : α) ↦ β a) (γ := γ) y

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : (a : α) → (b : β a) → Mul (γ a b)
x y : (a : α) → (b : β a) → γ a b
⊢ uncurry (β := β) (γ := γ) (x * y) = uncurry (β := β) (γ := γ) x * uncurry (β := β) (γ := γ) y

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : (a : α) → (b : β a) → Inv (γ a b)
x : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ) x⁻¹ = (curry (β := fun (a : α) ↦ β a) (γ := γ) x)⁻¹

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : (a : α) → (b : β a) → Inv (γ a b)
x : (a : α) → (b : β a) → γ a b
⊢ uncurry (β := β) (γ := γ) x⁻¹ = (uncurry (β := β) (γ := γ) x)⁻¹

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
inst_2 : (a : α) → (b : β a) → One (γ a b)
i : (a : α) × β a
x : γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
⊢ Eq (α := (x : α) → (y : β x) → γ x y)
    (curry (β := fun (a : α) ↦ β a) (γ := γ)
      (Pi.mulSingle (M := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
        i x))
    (Pi.mulSingle (M := fun (j : α) ↦ (y : β j) → γ j y) (i.fst (β := fun (a : α) ↦ β a))
      (Pi.mulSingle (M := γ (i.fst (β := fun (a : α) ↦ β a))) (i.snd (β := fun (a : α) ↦ β a)) x))

Tactic:
simp only [Pi.mulSingle, Sigma.curry_update, Sigma.curry_one, Pi.one_apply]

Premises used: Sigma.curry_update, Pi.one_apply, Sigma.curry_one, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
inst_2 : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
rw :
  Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
    (uncurry (β := β) (γ := γ)
      (curry (β := fun (a : α) ↦ β a) (γ := γ)
        (Pi.mulSingle (M := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) (mk (β := fun (a : α) ↦ β a) a b) x)))
    (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
rw₁ rw₂ :
  Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
    (Pi.mulSingle (M := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
      (mk (β := fun (a : α) ↦ β a) a b) x)
    (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
⊢ Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
    (uncurry (β := β) (γ := γ) (Pi.mulSingle (M := fun (x : α) ↦ (y : β x) → γ x y) a (Pi.mulSingle (M := γ a) b x)))
    (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)

Tactic:
rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]

Premises used: Sigma.uncurry_curry, Sigma.mk, Sigma.curry_mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
simp_rw :
  (∃ (b : (i : ι) → M i), ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔
    ∀ (i : ι), ∃ (b : M i), x i * b = 1 ∧ b * x i = 1
⊢ IsUnit x ↔ ∀ (i : ι), IsUnit (x i)

Tactic:
simp_rw [isUnit_iff_exists, funext_iff, ← forall_and]

Premises used: isUnit_iff_exists, funext_iff, forall_and
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ (b : (i : ι) → M i), ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔
    ∀ (i : ι), ∃ (b : M i), x i * b = 1 ∧ b * x i = 1

Tactic:
Classical.skolem (p := fun i y ↦ x i * y = 1 ∧ y * x i = 1).symm

Premises used: Classical.skolem, Iff.symm
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ (b : (i : ι) → M i), ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔
    ∀ (i : ι), ∃ (b : M i), x i * b = 1 ∧ b * x i = 1

Tactic:
exact Classical.skolem (p := fun i y ↦ x i * y = 1 ∧ y * x i = 1).symm

Premises used: Classical.skolem, Iff.symm
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
inst_1 : ∀ (i : ι), Subsingleton.{u_2 + 1} (M i)ˣ
⊢ ∀ (a : (i : ι) → M i), IsUnit a → a = 1

Tactic:
simp [Pi.isUnit_iff, funext_iff]

Premises used: funext_iff, Pi.isUnit_iff
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
rw : (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i)⁻¹ : M i) = (↑⋯.unit⁻¹ : M i)
⊢ (↑hx.unit⁻¹ : (i : ι) → M i) i = (↑⋯.unit⁻¹ : M i)

Tactic:
rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]

Premises used: Units.inv_eq_val_inv, MulEquiv.val_inv_piUnits_apply
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
e_self : (MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i = ⋯.unit
⊢ (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i)⁻¹ : M i) = (↑⋯.unit⁻¹ : M i)

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
e_self : (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i) : M i) = (↑⋯.unit : M i)
⊢ (MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i = ⋯.unit

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Units
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i) : M i) = (↑⋯.unit : M i)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
a : α
⊢ Membership.mem (γ := Finset α) 1 a ↔ a = 1

Tactic:
mem_singleton

Premises used: Finset.mem_singleton, Set.Mem, setOf
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ (↑1 : Set α) = 1

Tactic:
coe_singleton 1

Premises used: Finset.coe_singleton, setOf, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
s : Finset α
⊢ (↑s : Set α) = 1 ↔ s = 1

Tactic:
coe_eq_singleton

Premises used: Finset.coe_eq_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
s : Finset α
⊢ 1 ⊆ s ↔ 1 ∈ s

Tactic:
singleton_subset_iff

Premises used: Set.Mem, setOf, Finset.singleton_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq (α := Finset α) {1} 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ Membership.mem (γ := Finset α) 1 1

Tactic:
mem_singleton_self _

Premises used: Finset.mem_singleton_self, Set.Mem, setOf
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ Finset.Nonempty.{u_2} (α := α) 1

Tactic:
⟨1, one_mem_one⟩

Premises used: Finset.one_mem_one, Exists.intro, Finset.Nonempty, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
f : α ↪ β
⊢ map f 1 = singleton (α := β) ((f : (a : α) → β) 1 : β)

Tactic:
map_singleton f 1

Premises used: Finset.map_singleton, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : DecidableEq β
f : α → β
⊢ image f 1 = {f 1}

Tactic:
image_singleton _ _

Premises used: Finset.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
s : Finset α
⊢ s ⊆ 1 ↔ s = ∅ ∨ s = 1

Tactic:
subset_singleton_iff

Premises used: Set.Mem, setOf, Finset.subset_singleton_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
s : Finset α
h : s.Nonempty
⊢ s ⊆ 1 ↔ s = 1

Tactic:
h.subset_singleton_iff

Premises used: Set.Mem, setOf, Finset.Nonempty.subset_singleton_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ card.{u_2} (α := α) 1 = 1

Tactic:
card_singleton _

Premises used: Finset.card_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq (α := (a : α) → Finset α) (⇑singletonOneHom : (a : α) → Finset α) singleton

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
a : α
⊢ Eq (α := Finset α) ((singletonOneHom : (a : α) → Finset α) a : Finset α) ({a} : Finset α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One α
s : Finset α
a : α
inst_1 : DecidableEq β
inst_2 : One β
inst_3 : FunLike F α β
inst_4 : OneHomClass F α β
f : F
rw : Eq (α := Finset β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) 1
rw₁ : Eq (α := Finset β) {1} 1
rw₂ rw₃ : Eq.{u_3 + 1} (α := Finset β) 1 1
⊢ Eq.{u_3 + 1} (α := Finset β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) 1) 1

Tactic:
rw [image_one, map_one, singleton_one]

Premises used: map_one, Finset.image_one, Finset.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : α → β
⊢ sup 1 f = f 1

Tactic:
sup_singleton

Premises used: Finset.sup_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : SemilatticeSup β
f : α → β
⊢ sup' 1 ⋯ f = f 1

Tactic:
rfl

Premises used: WithBot.unbot, Finset.sup', rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : SemilatticeInf β
inst_2 : OrderTop β
f : α → β
⊢ inf 1 f = f 1

Tactic:
inf_singleton

Premises used: Finset.inf_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : SemilatticeInf β
f : α → β
⊢ inf' 1 ⋯ f = f 1

Tactic:
rfl

Premises used: Finset.inf', WithTop.untop, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
inst_1 : LinearOrder α
⊢ Eq.{u_2 + 1} (α := WithBot α) (Finset.max 1) 1

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.max, Finset.sup, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
inst_1 : LinearOrder α
⊢ Eq.{u_2 + 1} (α := WithTop α) (Finset.min 1) 1

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.min, Finset.inf, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
inst_1 : LinearOrder α
⊢ Eq.{u_2 + 1} (α := α) (max' 1 ⋯) 1

Tactic:
rfl

Premises used: Finset.max', WithBot.unbot, Finset.sup', rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
inst_1 : LinearOrder α
⊢ Eq.{u_2 + 1} (α := α) (min' 1 ⋯) 1

Tactic:
rfl

Premises used: Finset.min', Finset.inf', WithTop.untop, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
inst_1 : DecidableEq α
⊢ Eq.{u_2 + 1} (α := Finset αᵐᵒᵖ) (image op 1) 1

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.cons, Multiset.ofList, List.pwFilter, List.foldr, Finset.image, rfl, ite
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq.{u_2 + 1} (α := Finset αᵐᵒᵖ) (map (Equiv.toEmbedding opEquiv) 1) 1

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.cons, Multiset.ofList, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
h : ∀ (a : α × β), a ∈ SProd.sprod (α := Finset α) (β := Finset β) 1 1 ↔ Membership.mem (γ := Finset (α × β)) 1 a
⊢ SProd.sprod (α := Finset α) (β := Finset β) 1 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
a : α × β
⊢ a ∈ SProd.sprod (α := Finset α) (β := Finset β) 1 1 ↔ Membership.mem (γ := Finset (α × β)) 1 a

Tactic:
simp [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ s⁻¹ = image (fun (x : α) ↦ x⁻¹) s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ image (fun (x : α) ↦ x⁻¹) s = s⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
x : α
⊢ x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x

Tactic:
mem_image

Premises used: Finset.mem_image, Set.Mem, setOf
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
a : α
ha : a ∈ s
⊢ a⁻¹ ∈ s⁻¹

Tactic:
mem_image_of_mem _ ha

Premises used: Set.Mem, setOf, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ #s⁻¹ ≤ #s

Tactic:
card_image_le

Premises used: Finset.card_image_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
⊢ Eq.{u_2 + 1} (α := Finset α) ∅⁻¹ ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, Multiset.ofList, List.pwFilter, List.foldr, Finset.image, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ s⁻¹.Nonempty ↔ s.Nonempty

Tactic:
image_nonempty

Premises used: Finset.image_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Premises used: Finset.image_eq_empty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s t : Finset α
h : s ⊆ t
⊢ s⁻¹ ⊆ t⁻¹

Tactic:
image_subset_image h

Premises used: Set.Mem, setOf, Finset.image_subset_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
a : α
⊢ Eq (α := Finset α) {a}⁻¹ {a⁻¹}

Tactic:
image_singleton _ _

Premises used: Finset.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
a : α
s : Finset α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Tactic:
image_insert _ _ _

Premises used: Finset.image_insert
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Inv α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s : Finset α
f : α → β
⊢ s⁻¹.sup f = s.sup fun (x : α) ↦ f x⁻¹

Tactic:
sup_image ..

Premises used: Finset.sup_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Inv α
inst_2 : SemilatticeSup β
s : Finset α
hs : s⁻¹.Nonempty
f : α → β
⊢ s⁻¹.sup' hs f = s.sup' ⋯ fun (x : α) ↦ f x⁻¹

Tactic:
sup'_image ..

Premises used: Finset.sup'_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Inv α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s : Finset α
f : α → β
⊢ s⁻¹.inf f = s.inf fun (x : α) ↦ f x⁻¹

Tactic:
inf_image ..

Premises used: Finset.inf_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Inv α
inst_2 : SemilatticeInf β
s : Finset α
hs : s⁻¹.Nonempty
f : α → β
⊢ s⁻¹.inf' hs f = s.inf' ⋯ fun (x : α) ↦ f x⁻¹

Tactic:
inf'_image ..

Premises used: Finset.inf'_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ image op s⁻¹ = (image op s)⁻¹

Tactic:
image_comm op_inv

Premises used: Finset.image_comm, MulOpposite.op_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Inv α
s : Finset α
⊢ map (Equiv.toEmbedding opEquiv) s⁻¹ = (map (Equiv.toEmbedding opEquiv) s)⁻¹

Tactic:
simp [map_eq_image, image_op_inv]

Premises used: Finset.image_op_inv, Finset.map_eq_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
a : α
⊢ a ∈ s⁻¹ ↔ a⁻¹ ∈ s

Tactic:
simp [mem_inv, inv_eq_iff_eq_inv]

Premises used: Finset.mem_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
p : α → Prop
inst_2 : DecidablePred p
h : ∀ (a : α), a ∈ ({x ∈ s | p x})⁻¹ ↔ a ∈ {x ∈ s⁻¹ | p x⁻¹}
⊢ ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
p : α → Prop
inst_2 : DecidablePred p
a : α
⊢ a ∈ ({x ∈ s | p x})⁻¹ ↔ a ∈ {x ∈ s⁻¹ | p x⁻¹}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
p : α → Prop
inst_2 : Fintype α
inst_3 : DecidablePred p
⊢ (↑{x : α | p x}⁻¹ : Set α) = {x : α | p x⁻¹}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
⊢ (↑s⁻¹ : Set α) = (↑s : Set α)⁻¹

Tactic:
coe_image.trans Set.image_inv_eq_inv

Premises used: setOf, Finset.coe_image, Set.image_inv_eq_inv, Eq.trans