mathlib-initiative/mathlib-tactics huggingface dataset:
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)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ b1 * a1 * (b2 * a2) = b1 * a1 * (b2 * a2)

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ ¬Disjoint ↑s ↑t ↔ ¬Disjoint ↑s ↑t

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f.sum single ∈ ⨆ a, (lsingle a).range

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f.sum single ∈ ⨆ a, (lsingle a).range
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ ⊥

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ ⊥
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ {a⁻¹ * b} = {a⁻¹ * b}

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ {b * a⁻¹} = {b * a⁻¹}

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ {a⁻¹} = {a⁻¹}

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ {b⁻¹} = {b⁻¹}

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ {a} = {a}

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ {b} = {b}

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑t
b : α
hb : b ∈ ↑t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial

Tactic:
exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = span R (⇑(lsingle a) '' s)

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = span R (⇑(lsingle a) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_1.single
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ s • single (u i) 1 ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
]

Goal state after:
case refine_1.single
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ s • single (u i) 1 ∈ span R (Set.range fun x ↦ single (u x) 1)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_1.add
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf : (lmapDomain R R u) f ∈ span R (Set.range fun x ↦ single (u x) 1)
hg : (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)
⊢ (lmapDomain R R u) f + (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
]

Goal state after:
case refine_1.add
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf : (lmapDomain R R u) f ∈ span R (Set.range fun x ↦ single (u x) 1)
hg : (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)
⊢ (lmapDomain R R u) f + (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ n * s)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a + -b } = { toFinsupp := a } - { toFinsupp := b }

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a + -b } = { toFinsupp := a } - { toFinsupp := b }
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ ∀ (y : α), single (u y) 1 ∈ ↑(lmapDomain R R u).range

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ ∀ (y : α), single (u y) 1 ∈ ↑(lmapDomain R R u).range
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
n : ℕ
⊢ { toFinsupp := a.toFinsupp ^ n }.toFinsupp = a.toFinsupp ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a = 0 ↔ a = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a = 1 ↔ a = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ a = 0 ↔ a = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ a = 1 ↔ a = 1

Tactic:
]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ L = ⊤ ↔ L = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ L = ⊥ ↔ L = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L
Module: Mathlib.Order.Sublattice

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
]

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ (∃ s, m ∈ ⨆ i ∈ s, ↑i) ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ (∃ s, m ∈ ⨆ i ∈ s, ↑i) ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ ¬a = a0 ∨ ¬b0 = b

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ ¬a = a0 ∨ ¬b0 = b
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[ℕ]
⊢ p.coeff.support = p.coeff.support

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.toFinsupp.coeff.support = p.toFinsupp.coeff.support

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ m = n ∧ a = b ∨ a = 0 ∧ b = 0 ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ m ∈ ⨆ x, ⨆ (_ : ⟨↑x, ⋯⟩ ∈ s), ↑x

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ m ∈ ⨆ x, ⨆ (_ : ⟨↑x, ⋯⟩ ∈ s), ↑x
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (monomial 0).toFun 1 = 1

Tactic:
simp [monomial_zero_one]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
hu' :
  { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' =
      { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 →
    { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' = { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∧
      { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' = { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial (n + 1)) 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ p * X ^ (n + 1) = p * X ^ (n + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * q * X ^ n = p * q * X ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial (n + 1)) r = (monomial (n + 1)) r

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (monomial (n + k)) r = (monomial (n + k)) r

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[ℕ]
⊢ ⇑p.coeff = ⇑p.coeff

Tactic:
]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * ((a0, b0).1 * ((a0, b0).2 * b⁻¹)) = a⁻¹ * (a0 * (b0 * b⁻¹)) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * ((a0, b0).1 * ((a0, b0).2 * b⁻¹)) = a⁻¹ * (a0 * (b0 * b⁻¹)) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
h : n ≠ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ (monomial (n + 1)) a = (monomial (n + 1)) a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ single n a = single n a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
⊢ C a * X = C a * X

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ single 1 a = single 1 a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure (⇑(toFinsuppIso R).symm.toAddEquiv '' {x | ∃ m r, x = single m r}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure (⇑(toFinsuppIso R).symm.toAddEquiv '' {x | ∃ m r, x = single m r}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ (single n a).coeff.support = {n}

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ (single n a).coeff.support = {n}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (single n a).coeff.support ⊆ {n}

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (single n a).coeff.support ⊆ {n}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ {1} = {1}

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ {n} = {n}

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ single n 1 = single n 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) a = (monomial n) a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ {1} = {1}

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp }.sum f = p.sum f + q.sum f

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp }.sum f = p.sum f + q.sum f
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c1 * (d2 * c2⁻¹)) = d1⁻¹ * (c1 * (d2 * c2⁻¹)) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2

Tactic:
]

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c1 * (d2 * c2⁻¹)) = d1⁻¹ * (c1 * (d2 * c2⁻¹)) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
a : R
⊢ motive (Polynomial.C a)

Tactic:
]

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
a : R
⊢ motive (Polynomial.C a)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih : motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive (Polynomial.C (p.coeff n) * X ^ n + ∑ x ∈ s, Polynomial.C (p.coeff x) * X ^ x)

Tactic:
]

Goal state after:
case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih : motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive (Polynomial.C (p.coeff n) * X ^ n + ∑ x ∈ s, Polynomial.C (p.coeff x) * X ^ x)
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: M : Type u_2
inst✝⁷ : AddCommMonoid M
R : Type u_3
S : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : DistribSMul S R
inst✝¹ : SMulCommClass R S M
inst✝ : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ (↑c⁻¹ • ↑c • f).invtSubmodule ≤ f.invtSubmodule

Tactic:
]

Goal state after:
M : Type u_2
inst✝⁷ : AddCommMonoid M
R : Type u_3
S : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : DistribSMul S R
inst✝¹ : SMulCommClass R S M
inst✝ : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ (↑c⁻¹ • ↑c • f).invtSubmodule ≤ f.invtSubmodule