mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

pp: case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : ¬Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))

Tactic:
rw [span_insert_eq_span hb₁] at hb₃

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m₁ m₂ m₁' m₂' : M
hr₁ : r₁ ≠ 0
hr₂ : r₂ ≠ 0
⊢ single m₁ r₁ + single m₂ r₂ = single m₁' r₁ + single m₂' r₂ ↔
    m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = m₂'

Tactic:
by
  simp [← coeff_inj, single_add_single_eq_single_add_single, *]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c

Tactic:
simp [mul_def, mul_add, sum_add, sum_add_index]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

pp: case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (f * g).coeff (a0 * b0) = f.coeff a0 * g.coeff b0

Tactic:
simp_rw [coeff_mul, sum, ← Finset.sum_product']

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (∑ x ∈ f.coeff.support ×ˢ g.coeff.support, if x.1 * x.2 = a0 * b0 then f.coeff x.1 * g.coeff x.2 else 0) =
    f.coeff a0 * g.coeff b0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ∀ (b : A × A),
    b.1 ∈ f.coeff.support ∧ b.2 ∈ g.coeff.support →
      b ≠ (a0, b0) → (if b.1 * b.2 = a0 * b0 then f.coeff b.1 * g.coeff b.2 else 0) = 0

pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ∀ (b : A × A),
    b.1 ∈ f.coeff.support ∧ b.2 ∈ g.coeff.support →
      b ≠ (a0, b0) → (if b.1 * b.2 = a0 * b0 then f.coeff b.1 * g.coeff b.2 else 0) = 0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
af : a0 ∉ f.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

pp: case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
·

Goal state after:
case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
af : a0 ∉ f.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H.inl
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h : g₁.coeff.support ∪ g₂.coeff.support = ∅
⊢ g₁ = g₂

pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
⊢ g₁ = g₂

Tactic:
·

Goal state after:
case H.inl
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h : g₁.coeff.support ∪ g₂.coeff.support = ∅
⊢ g₁ = g₂
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ a * x.coeff 1 = 1

pp: case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ a * x.coeff 1 = 1
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ (a • x) • y = a • x • y

Tactic:
by simp only [smul_def, smul_eq_mul, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ (a • x) • y = a • x • y

Tactic:
by simp only [smul_def, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ a ∈ s.sort r ↔ a ∈ s

Tactic:
← mem_coe,

Goal state after:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ a ∈ ↑(s.sort r) ↔ a ∈ s
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
⊢ p1 = p2

pp: case refine_2
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
⊢ p1 = p2
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
Module: Mathlib.Data.Finset.Sort

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

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

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ ≤ s.min' H
Module: Mathlib.Data.Finset.Sort

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

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ s.min' H ≤ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

pp: case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
·

Goal state after:
case mp.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case a
α : 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
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] ≤ s.max' H

pp: case a
α : 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
l : List α := ⋯
⊢ s.max' H ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]

Tactic:
·

Goal state after:
case a
α : 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
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] ≤ s.max' H
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

Tactic:
·

Goal state after:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case a
α : 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
l : List α := ⋯
⊢ s.max' H ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]

Tactic:
·

Goal state after:
case a
α : 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
l : List α := ⋯
⊢ s.max' H ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
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
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

pp: case neg
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
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
·

Goal state after:
case pos
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
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
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:
← mem_coe,

Goal state after:
α : 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
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s

pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ #s ≤ #(image f univ)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ #s ≤ #(image f univ)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ #s ≤ #(image f univ)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refl.inl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b2 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b = (fun x ↦ a * x) b2
this : b ∈ {b, b2}
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2

pp: case refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
·

Goal state after:
case refl.inl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b2 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b = (fun x ↦ a * x) b2
this : b ∈ {b, b2}
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
·

Goal state after:
case refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case convert_3
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
x : Fin k
⊢ (i.succAbove ∘ Fin.cast ?convert_7) x ∈ {i}ᶜ

pp: case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n

Tactic:
·

Goal state after:
case convert_3
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
x : Fin k
⊢ (i.succAbove ∘ Fin.cast ?convert_7) x ∈ {i}ᶜ
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n

Tactic:
·

Goal state after:
case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n
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
  simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]

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

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

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a