mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
⊢ UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ (↑(s.sort r)).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ f a * f b = f a0 * f b0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ s.sort r ~ s.toList

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.toFinset.sort r = l ↔ List.Pairwise r l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
x✝¹ x✝ : H
⊢ x✝¹ ∈ image (⇑f) A → x✝ ∈ image (⇑f) B → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (cons a s h₂).sort r = a :: s.sort r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (insert a s).sort r = a :: s.sort r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (map f A) (map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul (map { toFun := op, inj' := ⋯ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)
a b : G
aA : a ∈ A
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
⊢ ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) (x✝¹ * x✝) =
    ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝¹ *
      ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : One α
s : Finset α
a : α
inst✝³ : DecidableEq β
inst✝² : One β
inst✝¹ : FunLike F α β
inst✝ : OneHomClass F α β
f : F
⊢ image (⇑f) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
⊢ 1 ×ˢ 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } A))
    (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } B)) (op (op a0)) (op (op b0))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Inv α
s : Finset α
⊢ map opEquiv.toEmbedding s⁻¹ = (map opEquiv.toEmbedding s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
a : α
⊢ a ∈ s⁻¹ ↔ a⁻¹ ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : InvolutiveInv α
p : α → Prop
inst✝¹ : Fintype α
inst✝ : DecidablePred p
⊢ ↑{x | p x}⁻¹ = {x | p x⁻¹}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(s.preimage (fun x ↦ x⁻¹) ⋯) = ↑s⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
⊢ univ⁻¹ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s t : Finset α
⊢ ↑(s ∩ t)⁻¹ = ↑(s⁻¹ ∩ t⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ map opEquiv.toEmbedding (s * t) = map opEquiv.toEmbedding t * map opEquiv.toEmbedding s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ = s.min' H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n✝ n : ℕ
hn : n + 1 ≠ 0
⊢ ∅ ^ (n + 1) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
⊢ (s ^ 0).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
⊢ 0 < #s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huH : UniqueMul (image (⇑f) A) (image (⇑f) B) aH bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ {a} ^ 0 = {a ^ 0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
n : ℕ
⊢ {a} ^ (n + 1) = {a ^ (n + 1)}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] = s.max' H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
by
  rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
  rfl

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
⊢ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ {x | x ∈ s.sort fun x1 x2 ↦ x1 ≤ x2} = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ #(s ^ 0) ≤ #s ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ Set.range ⇑(s.orderEmbOfFin h) = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ image (⇑(s.orderEmbOfFin h)) univ = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ map (s.orderEmbOfFin h).toEmbedding univ = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (fun t ↦ Bool.rec { down := (x * y).1 } { down := (x * y).2 } t) =
    (fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ k = (s.sort fun a b ↦ a ≤ b).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ List.map (⇑(s.orderEmbOfFin h)) (List.finRange k) = s.sort fun a b ↦ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) * #s ≤ #s ^ n * #s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ ({a}.orderEmbOfFin ⋯) i = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ (n + 1)) ≤ #s ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid α
n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ ↑(univ ^ n) = ↑univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ image op (s ^ 0) = image op s ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f = ⇑(s.orderEmbOfFin h)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : #s = k
h' : #s = l
⊢ (s.orderEmbOfFin h) i = (s.orderEmbOfFin h') j ↔ ↑i = ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b2
⊢ b1 = b2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ #s
a : Fin k
⊢ (s.orderEmbOfCardLe h) a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩

Goal state after:
G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ a = a1 ∧ b = b2
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ map opEquiv.toEmbedding (s ^ 0) = map opEquiv.toEmbedding s ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ {i}ᶜ.orderEmbOfFin h = RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
n : ℕ
i : Fin (n + 1)
⊢ #{i}ᶜ = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ map opEquiv.toEmbedding (s ^ (n + 1)) = map opEquiv.toEmbedding s ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
⊢ s ×ˢ t ^ 0 = (s ^ 0) ×ˢ (t ^ 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ #{i}ᶜ = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ ({i}ᶜ.orderEmbOfFin h) j = i.succAbove (Fin.cast ⋯ j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
⊢ ∀ (a : Fin n), (a ∈ Finset.univ.sort fun a b ↦ a ≤ b) ↔ a ∈ List.finRange n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
⊢ Nonempty (α ↪o β)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Fintype

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
inst✝¹ : Zero α
inst✝ : Fintype α
⊢ card (ι →₀ α) = card α ^ card ι

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
m : R'
x : M'
i : I
⊢ (e.toFun (m • x)) i = ((RingHom.id R') m • e.toFun x) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
⊢ Free R' M'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
⊢ B.repr ((algebraMap R S) r) = Finsupp.single i r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit ↑s ↔ IsUnit s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : DivisionMonoid α
inst✝ : Fintype α
⊢ univ / univ = univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
⊢ (∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x) →
    ∀ (g : End R M) (x : M), g (f x) = f (g x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Subsingleton M
⊢ ∀ (g : R), g * 0 = 0 * g

Tactic:
by

Goal state after: