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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * ∏ m ∈ insert a (s.toFinset.erase a), f m ^ count m s =
    ∏ x ∈ insert a (s.toFinset.erase a), f x ^ count x (a :: s)

Tactic:
prod_insert (notMem_erase _ _),

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * (f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s) =
    ∏ x ∈ insert a (s.toFinset.erase a), f x ^ count x (a :: s)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * (f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s) =
    ∏ x ∈ insert a (s.toFinset.erase a), f x ^ count x (a :: s)

Tactic:
prod_insert (notMem_erase _ _),

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * (f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s) =
    f a ^ count a (a :: s) * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
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:
by 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
x : G
hx : x ∈ N
⊢ (f x)⁻¹ * 1 ∈ M

Tactic:
mul_one,

Goal state after:
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
x : G
hx : x ∈ N
⊢ (f x)⁻¹ ∈ M
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_1
G : Type u_3
inst✝ : Group G
x✝ : FG G
S : Finset G
hS : Subgroup.closure ↑S = ⊤
⊢ Function.Surjective ⇑(FreeGroup.lift Subtype.val)

Tactic:
← MonoidHom.range_eq_top,

Goal state after:
case refine_1
G : Type u_3
inst✝ : Group G
x✝ : FG G
S : Finset G
hS : Subgroup.closure ↑S = ⊤
⊢ (FreeGroup.lift Subtype.val).range = ⊤
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ * ↑⟨1, hs⟩ = x✝ * ↑⟨1, hs⟩
⊢ ↑⟨1, hs⟩ * x✝¹ = ↑⟨1, hs⟩ * x✝

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ = x✝ * ↑⟨1, hs⟩
⊢ ↑⟨1, hs⟩ * x✝¹ = ↑⟨1, hs⟩ * x✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case e_f
M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
j : κ
⊢ ∏ _i, f j = ∏ i with g i = j, f j

Tactic:
exact (prod_subtype _ (by simp) fun _ ↦ _).symm

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∃ u, s = k • u

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(BigOperators.bigsum
   "∑"
   (BigOperators.bigOpBinders (BigOperators.bigOpBinder `a [(Lean.«binderPred∈_» "∈" `s.toFinset)]))
   []
   ","
   («term_•_»
    (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) («term_/_» (Term.app `s.count [`a]) "/" `k) ")")
    "•"
    (choice
     («term{_}» "{" [`a] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `a []) [])])
      (Term.optEllipsis [])
      []
      "}"))))])

Goal state after:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
⊢ ⁅H, K⁆ ≤ K

pp: case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
· exact commutator_le.mpr fun h hh k hk ↦ mul_mem (hH h hh k hk) (inv_mem hk)

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ x * -of L2 * of L3 = x * -(of L2 * of L3)

Tactic:
mul_neg,

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ -(x * of L2) * of L3 = x * -(of L2 * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ -(x * of L2) * of L3 = x * -(of L2 * of L3)

Tactic:
mul_neg,

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ -(x * of L2) * of L3 = -(x * (of L2 * of L3))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ x * y * -of L3 = x * (y * -of L3)

Tactic:
mul_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * y * of L3) = x * (y * -of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * y * of L3) = x * (y * -of L3)

Tactic:
mul_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * y * of L3) = x * -(y * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * y * of L3) = x * -(y * of L3)

Tactic:
mul_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * y * of L3) = -(x * (y * of L3))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
⊢ (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)

Tactic:
induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ (lift ⇑f) (x * -of L2) = (lift ⇑f) x * (lift ⇑f) (-of L2)

Tactic:
mul_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ (lift ⇑f) (-(x * of L2)) = (lift ⇑f) x * (lift ⇑f) (-of L2)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (x * of L2) = (lift ⇑f) x * -(lift ⇑f) (of L2)

Tactic:
mul_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (x * of L2) = -((lift ⇑f) x * (lift ⇑f) (of L2))
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ Function.Surjective ⇑((QuotientGroup.mk' N).comp H.subtype)

Tactic:
← MonoidHom.range_eq_top,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ ((QuotientGroup.mk' N).comp H.subtype).range = ⊤
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
ih : of s * of t = of t * of s
⊢ of s * -of t = -of t * of s

Tactic:
mul_neg,

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
ih : of s * of t = of t * of s
⊢ -(of s * of t) = -of t * of s
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ↑(t₂ * t₁) * (↑(b * d).2 * (a * c).1) = ↑(t₂ * t₁) * (↑(a * c).2 * (b * d).1)

Tactic:
calc
      (t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_rfl

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Tactic:
· rintro ⟨u, hu, v, e₁, e₂⟩
    exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp.mp
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)
H : Injective ⇑(f.lift hg)
x y : M
⊢ f x = f y → g x = g y

pp: case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
⊢ g x = g y → f x = f y

Tactic:
· exact f.eq_of_eq hg

Goal state after:
case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
⊢ g x = g y → f x = f y
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ i (z * f ↑x) = i (f w')

Tactic:
← hxw,

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ i (z * f ↑x) = i (w * f ↑x)
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
z : Q
⊢ ∃ a, (f.map hy k) a = z

Tactic:
obtain ⟨y, ⟨t, ht⟩, rfl⟩ := k.mk'_surjective z

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
y t : P
ht : t ∈ T
⊢ ∃ a, (f.map hy k) a = k.mk' y ⟨t, ht⟩
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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ (∃ c, ↑c * k x = ↑c * k y) → ∃ c, ↑c * x = ↑c * y

Tactic:
rintro ⟨c, hc⟩

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 : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : ↑c * k x = ↑c * k y
⊢ ∃ c, ↑c * x = ↑c * y
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
P : Type u_3
inst✝ : CommMonoid P
y : ↥S
⊢ mk (↑y * 1) (1 * y) = 1

Tactic:
mul_one,

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
y : ↥S
⊢ mk (↑y) (1 * y) = 1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤

pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝

Tactic:
· rw [mul_top ha, untopD_top, mul_zero]

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ oreNum r s✝ • r✝ /ₒ (oreDenom r s✝ * 1) = oreNum (r • 1) s✝ • r✝ /ₒ oreDenom (r • 1) s✝

Tactic:
mul_one,

Goal state after:
case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ oreNum r s✝ • r✝ /ₒ oreDenom r s✝ = oreNum (r • 1) s✝ • r✝ /ₒ oreDenom (r • 1) s✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

Tactic:
· simp [hc]

Goal state after:
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

Tactic:
· simp [hc]

Goal state after:
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x

Tactic:
apply hf.seq_le_seq n
  · rfl
  · intros; rw [iterate_succ_apply']
  · simp [h.iterate_right _ _, hg.iterate _ hx]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ ≤ v₂ ∨ v₂ ≤ v₁

Tactic:
by
  obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate
  obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate
  clear h₁ h₂
  wlog h : n ≤ m
  · rw [Or.comm]
    apply this
    exact Nat.le_of_not_ge h
  left
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [Nat.add_comm, Function.iterate_add, Function.comp_apply]
  apply Order.le_succ_iterate

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
h : ¬IsMax b
⊢ b ⋖ succ b

Tactic:
exact covBy_succ_of_not_isMax h

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ n, pred^[n] b = a

Tactic:
refine (exists_pred_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∀ (a_1 : ℕ), pred^[a_1] (EquivLike.inv f b) = EquivLike.inv f a → pred^[a_1] b = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
a : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a < succ ⊥ ↔ a = ⊥

Tactic:
lt_succ_iff,

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
a : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a ≤ ⊥ ↔ a = ⊥
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : IsMax a✝
⊢ IsMax ↑a✝

Tactic:
← succ_eq_iff_isMax

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : succ a✝ = a✝
⊢ IsMax ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b : ℕ∞
h : a + b < ⊤
⊢ (a + b).lift h = a.lift ⋯ + b.lift ⋯

Tactic:
apply natCast_inj.1

Goal state after:
a b : ℕ∞
h : a + b < ⊤
⊢ ↑((a + b).lift h) = ↑(a.lift ⋯ + b.lift ⋯)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h : ⟨x, hx⟩ ≤ ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
· rintro ⟨y, hy⟩ h
      rcases h.lt_or_eq with h | h
      · simp only [Subtype.mk_lt_mk] at h
        have := h.le_pred
        absurd h'
        apply out' hy hx
        simp [this, Order.pred_le]
      · simp [h]

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ IsMin a

Tactic:
rw [← pred_eq_iff_isMin]
  change dite .. = _
  simp [h]

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ IsMax a

Tactic:
← succ_eq_iff_isMax

Goal state after:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ succ a = a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (∏ j, if h : j = i then f j h else 1) = f i ⋯

Tactic:
rw [Finset.prod_dite_eq', if_pos (mem_univ _)]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : AddConst α (α✝ → β✝)
x✝ : α✝
⊢ x✝¹ <*> pure x✝ = (fun h ↦ h x✝) <$> x✝¹

Tactic:
simp [Const.map, map, Seq.seq, pure, add_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ p a

Tactic:
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ p a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ ∀ (x : α), x ∈ v.toList → p x

Tactic:
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ ∀ (x : α), x ∈ v.toList → p x
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Sort u
⊢ Uncountable α ↔ IsEmpty (α ↪ ℕ)

Tactic:
← not_countable_iff,

Goal state after:
α : Sort u
⊢ ¬Countable α ↔ IsEmpty (α ↪ ℕ)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter (fun x ↦ a ≠ x) ↑m + ↑(replicate (↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.fst) a) = ↑m

Tactic:
Fin.val_mk

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter (fun x ↦ a ≠ x) ↑m + ↑(replicate (count a ↑m) a) = ↑m