mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ s.IsPWO

Tactic:
IsPWO,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ s.PartiallyWellOrderedOn fun x1 x2 ↦ x1 ≤ x2
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z

Tactic:
exact ⟨y, hy, z, hzB, rfl⟩

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

Goal state before:
pp: case e_b
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ 1 = Multiset.foldr (fun x1 x2 ↦ x1 * x2) 1 (Multiset.map (fun i ↦ 1) s.val)

Tactic:
exact prod_const_one.symm

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ ∏ x ∈ (map Embedding.inl s).disjUnion (map Embedding.inr t) ⋯, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
prod_disjUnion,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ (∏ x ∈ map Embedding.inl s, f x) * ∏ x ∈ map Embedding.inr t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ IsReduced ((a₁, b₁) :: (a₂, b₂) :: L₁)

Tactic:
by
    rw [isReduced_cons_cons]
    refine ⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩
    rintro rfl
    symm
    rw [← Bool.ne_not]
    rintro rfl
    exact hL₁ L₁ <| .not (L₁ := [])

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∉ {a ∈ s | p a}
⊢ (if p x then f x else 1) = 1

Tactic:
rw [mem_filter, not_and] at h

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ (if p x then f x else 1) = 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, g x = (map f) x

Tactic:
rintro ⟨L⟩
  exact List.recOn L g.map_one fun ⟨x, b⟩ t (ih : g (FreeGroup.mk t) = map f (FreeGroup.mk t)) =>
    Bool.recOn b
      (show g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) =
          FreeGroup.map f ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) by
        simp [g.map_mul, g.map_inv, hg, ih])
      (show g (FreeGroup.of x * FreeGroup.mk t) =
          FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by simp [g.map_mul, hg, ih])

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)
⊢ ∏ x ∈ range (n + (m + 1)), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range (m + 1), f (n + x)

Tactic:
Nat.add_succ,

Goal state after:
case succ
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)
⊢ ∏ x ∈ range (n + m).succ, f x = (∏ x ∈ range n, f x) * ∏ x ∈ range (m + 1), f (n + x)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
⊢ FG M'

Tactic:
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›

Goal state after:
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
s : List M
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ count m s

Tactic:
simpa using prod_list_map_count s id

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M✝ : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Monoid M✝
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ G ⧸ N →* H ⧸ M

Tactic:
by
  refine QuotientGroup.lift N ((mk' M).comp f) ?_
  intro x hx
  refine QuotientGroup.eq.2 ?_
  rw [mul_one, Subgroup.inv_mem_iff]
  exact h hx

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ t ∪ s, f x = ∏ x ∈ s ∪ t, f x

Tactic:
union_comm

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ s ∪ t, f x = ∏ x ∈ s ∪ t, f x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f (g₁ * g₂ * g₁⁻¹ * g₂⁻¹) = f g₁ * f g₂ * (f g₁)⁻¹ * (f g₂)⁻¹

Tactic:
map_mul f,

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f g₁ * f g₂ * f g₁⁻¹ * f g₂⁻¹ = f g₁ * f g₂ * (f g₁)⁻¹ * (f g₂)⁻¹
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

Tactic:
simp_rw [commutatorElement_def, map_mul f, map_inv f]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> (y₁ + y₂) = (fun b a ↦ (a, b)) <$> (y₁ + y₂) <*> pure p

Tactic:
| add y₁ y₂ ih1 ih2 =>

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
a : M
s : Finset ι
m : ι → Multiset M
⊢ a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i

Tactic:
by
  induction s using Finset.cons_induction with grind

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

Goal state before:
pp: M : Type u_4
ι : Type u_5
inst✝ : CommMonoid M
f : ι → Multiset M
s : Finset ι
⊢ (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod

Tactic:
by
  induction s using Finset.cons_induction with grind

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
⊢ IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)

Tactic:
by
  induction s using Finset.cons_induction with grind

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs

Tactic:
by
  induction s using Finset.cons_induction with grind

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ commutator G = ⊥ ↔ IsMulCommutative G

Tactic:
rw [commutator_eq_bot_iff_center_eq_top, center_eq_top_iff]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z

Tactic:
| _ r₂ s₂
   => 

Goal state after:
case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : k z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ v * k (f ↑x.2) = k (f x.1)

Tactic:
← hx,

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : k z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ v * k (f ↑x.2) = k (z * f ↑x.2)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f (↑y₂ * x₁) = f (↑y₁ * x₂)

Tactic:
map_mul f,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f ↑y₂ * f x₁ = f (↑y₁ * x₂)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f ↑y₂ * f x₁ = f (↑y₁ * x₂)

Tactic:
map_mul f,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f ↑y₂ * f x₁ = f ↑y₁ * f x₂
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f (x₁ * ↑y₂) * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹

Tactic:
map_mul f,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f x₁ * f ↑y₂ * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b

Tactic:
· exact succ_le_iff_of_not_isMax ha

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
this : ¬IsMin a
⊢ ¬IsMin ↑a

Tactic:
rw [not_isMin_iff] at ⊢ this

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
this : ∃ b, b < a
⊢ ∃ b, b < ↑a
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ succ x ≤ y

Tactic:
exact succ_le_of_lt h

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_gt a

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
c : α
hc : a < c
⊢ False
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v)

Tactic:
by
  ext j
  rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ StrictMono f

Tactic:
simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i

Tactic:
prod_eq_mul_prod_sdiff_singleton_of_mem hi,

Goal state after:
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ f i * ∏ x ∈ s \ {i}, f x = ∏ j ∈ s, g j ↔ f i = g i

Tactic:
prod_eq_mul_prod_sdiff_singleton_of_mem hi,

Goal state after:
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ f i * ∏ x ∈ s \ {i}, f x = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑(fill a (filterNe a m).fst (filterNe a m).snd) = ↑m

Tactic:
rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
      ext b; dsimp
      rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
      obtain rfl | h := eq_or_ne a b
      · rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
      · rw [if_pos h, if_neg h, add_zero]

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) ↑m.snd + filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a) = ↑m.snd

Tactic:
filter_eq_self.2,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑m.snd + filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a) = ↑m.snd

α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (List.Vector α n) = Fintype.card α ^ n

Tactic:
rw [Fintype.ofEquiv_card]; simp

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable ↑s
⊢ (⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable

Tactic:
rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (map₂ f (a✝ ::ᵥ x✝) (b✝ ::ᵥ y✝)).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
rw [map₂_cons]

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : (α ⊕ₗ β)ᵒᵈ
⊢ (Equiv.sumComm α β) a ≤ (Equiv.sumComm α β) b ↔ a ≤ b

Tactic:
rcases a with (a | a)

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
b : (α ⊕ₗ β)ᵒᵈ
a : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) b ↔ inl a ≤ b

case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
b : (α ⊕ₗ β)ᵒᵈ
a : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) b ↔ inr a ≤ b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ ⊤

Tactic:
simp only [lex_inr_inr, le_top]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds (bot x f)

Tactic:
intro y hy

Goal state after:
case right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
⊢ x ≤ y
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ++ mb ∈ a ++ b

Tactic:
by simp [append_def]; aesop

Goal state after:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : g' (g x') = g' (g y')
⊢ g x' = g y'

Tactic:
rw [g'g _, g'g _] at hxy

Goal state after:
case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Tactic:
zero_power h

Goal state after:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ≤ 1
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat (lift.{v, u} c) = toENat c

Tactic:
by
  cases le_total c ℵ₀ with
  | inl ha => lift c to ℕ∞ using ha; simp
  | inr ha => simp [toENat_eq_top.2, ha]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)

Tactic:
by rwa [mul_comm]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0

Tactic:
rcases h with rfl | ⟨a, ha, rfl⟩

Goal state after:
case refine_2.inl
⊢ sInf ∅ = 0

case refine_2.inr
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card

Tactic:
· obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n
    exact ⟨s, hs.symm⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
ha : ↑n < ℵ₀
⊢ ↑n + 1 < ℵ₀

Tactic:
← Nat.cast_add_one

Goal state after:
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(n + 1) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n

Tactic:
· rintro ⟨t, rfl, rfl⟩
    exact mk_coe_finset

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
h' : #↑(T \ S) = 0
⊢ #↑(T \ S) + #↑S ≤ #↑S

Tactic:
simp [h']

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑2 + 1 ≤ #α

Tactic:
← Nat.cast_add_one

Goal state after:
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑(2 + 1) ≤ #α
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)

Tactic:
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ f (x✝¹ • m) = f (x✝ • m)

Tactic:
by simp_rw [map_smul, h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Opposite

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
by
    cases subsingleton_or_nontrivial α
    · exact Subsingleton.elim ..
    · exact unop_injective <| mul_left_cancel₀ one_ne_zero (h 1)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact DFunLike.congr_fun h a

Goal state after: