mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (r : R), ((mapRingHom M ↑e.symm).comp (mapRingHom M ↑e)) (single 1 r) = (RingHom.id R[M]) (single 1 r)

pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (m : M), ((mapRingHom M ↑e.symm).comp (mapRingHom M ↑e)) (single m 1) = (RingHom.id R[M]) (single m 1)

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (r : R), ((mapRingHom M ↑e.symm).comp (mapRingHom M ↑e)) (single 1 r) = (RingHom.id R[M]) (single 1 r)

case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (m : M), ((mapRingHom M ↑e.symm).comp (mapRingHom M ↑e)) (single m 1) = (RingHom.id R[M]) (single m 1)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∈ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

pp: case neg
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∉ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

Tactic:
<;>

Goal state after:
case pos
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∈ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

case neg
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∉ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ f = (f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom

pp: case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ g = (g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ f = (f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom

case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ g = (g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ f x✝ = ((f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝

pp: case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ g x✝ = ((g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ f x✝ = ((f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝

case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ g x✝ = ((g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
u : Finset V
h : ↑u ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑u ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
exact
    ⟨u, Subset.trans h.1 (by simp +contextual [subset_def, or_imp]),
      h.2.1, by simp only [h.2.2, eq]⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (x y : R[M]ᵐᵒᵖ),
    (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun (x * y) =
      (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun x *
        (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun y

Tactic:
classical
    simp [coeff_mul, MonoidAlgebra.ext_iff, Finsupp.ext_iff, ← MulOpposite.unop_inj,
      unop_finsuppSum, sum_mapRange_index, apply_ite unop, mapAddEquiv]
    simpa using fun _ _ _ ↦ Finsupp.sum_comm ..

Goal state after:
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 ∈ f.coeff.support ×ˢ 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, b0) ∉ f.coeff.support ×ˢ g.coeff.support →
    (if (a0, b0).1 * (a0, b0).2 = a0 * b0 then f.coeff (a0, b0).1 * g.coeff (a0, b0).2 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 ∈ f.coeff.support ×ˢ 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

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, b0) ∉ f.coeff.support ×ˢ g.coeff.support →
    (if (a0, b0).1 * (a0, b0).2 = a0 * b0 then f.coeff (a0, b0).1 * g.coeff (a0, b0).2 else 0) = 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
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]},
      (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂ → g₁.coeff.support ∪ g₂.coeff.support = s.erase s_1 → g₁ = g₂
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
hg : g₁.coeff.support ∪ g₂.coeff.support = s
h : s = ∅
⊢ 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
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]},
      (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂ → g₁.coeff.support ∪ g₂.coeff.support = s.erase s_1 → g₁ = g₂
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
hg : g₁.coeff.support ∪ g₂.coeff.support = s
h : s.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
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]},
      (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂ → g₁.coeff.support ∪ g₂.coeff.support = s.erase s_1 → g₁ = g₂
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
hg : g₁.coeff.support ∪ g₂.coeff.support = s
h : s = ∅
⊢ g₁ = g₂

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
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]},
      (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂ → g₁.coeff.support ∪ g₂.coeff.support = s.erase s_1 → g₁ = g₂
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
hg : g₁.coeff.support ∪ g₂.coeff.support = s
h : s.Nonempty
⊢ g₁ = g₂
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
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
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ {a ∈ A | f a = aH}

pp: case refine_2
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
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ {b ∈ B | f b = bH}

Tactic:
<;>

Goal state after:
case refine_1
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
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ {a ∈ A | f a = aH}

case refine_2
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
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ {b ∈ B | f b = bH}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

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

Tactic:
<;>

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

case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

pp: case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ t

Tactic:
<;>

Goal state after:
case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ s

case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ t
Module: Mathlib.Algebra.Group.UniqueProds.Basic

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

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

Tactic:
<;>

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

case true
G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (Bool.rec { down := (x * y).1 } { down := (x * y).2 } true).down =
    (((fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t)
        true).down
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case ofNat
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.ofNat a✝ ≠ 0
⊢ ∅ ^ Int.ofNat a✝ = ∅

pp: case negSucc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.negSucc a✝ ≠ 0
⊢ ∅ ^ Int.negSucc a✝ = ∅

Tactic:
<;>

Goal state after:
case ofNat
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.ofNat a✝ ≠ 0
⊢ ∅ ^ Int.ofNat a✝ = ∅

case negSucc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.negSucc a✝ ≠ 0
⊢ ∅ ^ Int.negSucc a✝ = ∅
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case ofNat
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.ofNat a✝ = {a ^ Int.ofNat a✝}

pp: case negSucc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.negSucc a✝ = {a ^ Int.negSucc a✝}

Tactic:
<;>

Goal state after:
case ofNat
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.ofNat a✝ = {a ^ Int.ofNat a✝}

case negSucc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.negSucc a✝ = {a ^ Int.negSucc a✝}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

pp: case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

pp: case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ (n + 1) } = npowRec (n + 1) { toFinsupp := a }

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s / s)

pp: case inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s / s)

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s / s)

case inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s / s)
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:
← Nat.cast_ofNat

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
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp =
    (∑ i ∈ p.support, ∑ x ∈ q.support, (monomial (i + x)) (p.toFinsupp.coeff i * q.toFinsupp.coeff x)).toFinsupp

Tactic:
toFinsupp_sum,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp =
    ∑ x ∈ p.support, ∑ i ∈ q.support, ((monomial (x + i)) (p.toFinsupp.coeff x * q.toFinsupp.coeff i)).toFinsupp
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 • f).invtSubmodule = f.invtSubmodule

Tactic:
apply le_antisymm ?_ (invtSubmodule_le_invtSubmodule_smul f c.1)
  grw [invtSubmodule_le_invtSubmodule_smul (c.1 • f) c⁻¹.1]
  simp [smul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
u : G
h✝ : u = s
⊢ (Pi.single s 1 * Pi.single x✝¹ 1) u = 0 u

pp: case neg
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
u : G
h✝ : ¬u = s
⊢ (Pi.single s 1 * Pi.single x✝¹ 1) u = 0 u

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
u : G
h✝ : u = s
⊢ (Pi.single s 1 * Pi.single x✝¹ 1) u = 0 u

case neg
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
u : G
h✝ : ¬u = s
⊢ (Pi.single s 1 * Pi.single x✝¹ 1) u = 0 u
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
t : G
h✝ : t = s
⊢ φ.toLinearMap ((Pi.basisFun k G) t) = (Pi.evalAlgHom k (fun i ↦ k) s).toLinearMap ((Pi.basisFun k G) t)

pp: case neg
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
t : G
h✝ : ¬t = s
⊢ φ.toLinearMap ((Pi.basisFun k G) t) = (Pi.evalAlgHom k (fun i ↦ k) s).toLinearMap ((Pi.basisFun k G) t)

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
t : G
h✝ : t = s
⊢ φ.toLinearMap ((Pi.basisFun k G) t) = (Pi.evalAlgHom k (fun i ↦ k) s).toLinearMap ((Pi.basisFun k G) t)

case neg
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
t : G
h✝ : ¬t = s
⊢ φ.toLinearMap ((Pi.basisFun k G) t) = (Pi.evalAlgHom k (fun i ↦ k) s).toLinearMap ((Pi.basisFun k G) t)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.1 = y.1

pp: case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.2 = y.2

Tactic:
<;>

Goal state after:
case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.1 = y.1

case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.2 = y.2