mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⇑φ

Tactic:
rw [MulHom.coe_coe, ← MonoidHom.range_eq_top, MonoidHom.range_eq_map, ← Subgroup.map_map, ← this,
    Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN, ← MonoidHom.range_eq_map]

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) ⊤ = ⊤
⊢ N ⊔ H.subtype.range = N ⊔ H ⊔ N
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
neg_mul,

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

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) (of default)) = of default →
    (fun n ↦ n • of default) ((lift fun x ↦ 1) (-of default)) = -of default

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑s' * ↑s ∈ S

Tactic:
by norm_cast; apply SetLike.coe_mem

Goal state after:
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)
x y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * g ↑c * g x = g y

Tactic:
rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * ↑s₂ ∈ S
⊢ 1 * ↑s₁ ∈ S

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f g : α ≃*o β
⊢ ∀ {a b : α}, (MulEquiv.refl α).toFun a ≤ (MulEquiv.refl α).toFun b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f✝ g✝ f : α ≃*o β
g : β ≃*o γ
⊢ ∀ {a b : α}, ((↑f).trans ↑g).toFun a ≤ ((↑f).trans ↑g).toFun b ↔ a ≤ b

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ 1 * ↑s₂ ∈ S

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x✝ : ↥S
⊢ ↑1 * (↑(↑x✝, x✝).2 * 1.1) = ↑1 * (↑1.2 * (↑x✝, x✝).1)

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * ↑y * p, t * y * q) = (↑t * ↑q * x, t * q * y)

Tactic:
simp_rw [mul_assoc, ht, mul_comm y q]

Goal state after:
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
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ ((k.lift hl).comp k.toMonoidHom) x = l x

Tactic:
lift_comp

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ l x = l x
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : WithZero G ≃*o WithZero H
a b : G
⊢ (MulEquiv.withZero.symm ↑e).toFun a ≤ (MulEquiv.withZero.symm ↑e).toFun b ↔ a ≤ b

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ⟨r, hr⟩ • 1 = 1 • r

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ ↑1 * r = r * ↑1

Tactic:
by simp

Goal state after:
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
k : S.LocalizationMap P
x : M
⊢ (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)) x = k x

Tactic:
by simp

Goal state after:
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
k : N ≃* P
x : N
⊢ (f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k)) x = k x

Tactic:
by simp

Goal state after:
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
f : S.LocalizationMap N
x : M
⊢ (mulEquivOfQuotient f) ((monoidOf S) x) = f x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
s s' : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s t : ↥S
⊢ ↑1 * (r₁ * ↑s) = r₁ * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s t : ↥S
⊢ ↑1 * (r₁ * ↑s) = r₁ * ↑s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
p : R
r : X
s : ↥S
⊢ ↑1 * p = p * ↑1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
p r : R
s : ↥S
⊢ ↑1 * p = p * ↑1

Tactic:
by simp

Goal state after:
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
x✝ y✝ : M
⊢ (∃ c, ↑c * (↑(y✝, 1).2 * (x✝, 1).1) = ↑c * (↑(x✝, 1).2 * (y✝, 1).1)) ↔ ∃ c, ↑c * x✝ = ↑c * y✝

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (n₁ * f (↑ms₁.2 * ↑ms₂.2)) = f m * (n₂ * f (↑ms₁.2 * ↑ms₂.2))
⊢ n₁ * f (↑ms₁.2 * ↑ms₂.2) = n₂ * f (↑ms₁.2 * ↑ms₂.2)

Tactic:
rw [map_mul, ← mul_assoc n₁, eq₁, ← mul_assoc n₂, mul_right_comm n₂, eq₂] at eq ⊢

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (f ms₂.1 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = f ms₂.1 * f ↑ms₁.2
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ ↑s₁ * r • 1 = r • 1 * ↑s₁

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
by
    rw [iterate_succ_apply']
    exact h _

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
x✝¹ : WithBot α
x✝ : ⊥ ≤ x✝¹
⊢ ⊥.succ ≤ x✝¹.succ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
hab : ⊥ < ↑b
⊢ ⊥.succ < (↑b).succ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
x✝¹ : WithTop α
x✝ : x✝¹ ≤ ⊤
⊢ x✝¹.pred ≤ ⊤.pred

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
hab : ↑b < ⊤
⊢ (↑b).pred < ⊤.pred

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
a : α
inst✝⁴ : Preorder α
inst✝³ : SuccOrder α
inst✝² : IsSuccArchimedean α
inst✝¹ : NoMaxOrder α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Iic a ⊆ Iio (succ a)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b

Tactic:
revert h
  refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
  have := hc.isMax.succ_eq
  rw [this] at hc ⊢
  exact H hc

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

Goal state before:
pp: α : Type u_1
a : α
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha : a ≠ ⊤
⊢ pred a ≠ ⊤

Tactic:
induction a <;> simp

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

Goal state before:
pp: n m : ℕ
⊢ ↑n < ↑m ↔ n < m

Tactic:
by simp

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

Goal state before:
pp: n m : ℕ
⊢ ↑n ≤ ↑m ↔ n ≤ m

Tactic:
by simp

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
N : Type u_2
inst✝ : One N
f : OneHom ℕ N
⊢ map (⇑f) 1 = 1

Tactic:
by simp

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
N : Type u_2
inst✝ : Zero N
f : ZeroHom ℕ N
⊢ map (⇑f) 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.Sigma

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : Fintype ι
⊢ ∀ (x : (i : ι) × κ i), x ∈ univ.sigma fun x ↦ univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ n - i + min n i = n

Tactic:
by simp

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ F1 = F2

Tactic:
by
      apply Functor.ext
      intros
      exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
⊢ ∀ {α : Type u} (x : α), id (pure x) = pure x

Tactic:
by simp

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ id (x <*> y) = id x <*> id y

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
⊢ (∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : α
⊢ (f <$> pure x).run = (pure (f x)).run

Tactic:
by simp

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

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

Tactic:
by
  rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ (m.erase a).card = n

Tactic:
by rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α n✝
a b : α
n : ℕ
f : α → β
x : Sym α n
⊢ (Multiset.map f ↑x).card = n

Tactic:
by simp

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 : ℕ
v : Vector α n
⊢ v.toList.reverse.length = n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
⊢ {a}.card = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
l : { x // x.length = 1 }
⊢ 0 < (↑l).length

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : Bool → α
⊢ ∏ b, f b = f true * f false

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_7
s : Finset α
n : ℕ
⊢ #(piFinset fun x ↦ s) = #s ^ n

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ (fun j ↦ a.get ⟨↑j, ⋯⟩) ∈ univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : a ∉ s
⊢ count a ↑(fill a i s) = ↑i

Tactic:
by
  simp [coe_fill, coe_replicate, hx]

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ ∀ (n : ℕ) (h₁ : n < (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).length) (h₂ : n < a.length),
    (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).get ⟨n, h₁⟩ = a.get ⟨n, h₂⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
⊢ decode (encode s) = s

Tactic:
by_cases h : none ∈ s
  · simp [h]
  · simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map,
      comp_apply, Option.some_get]
    convert! s.attach_map_coe

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Unique α
u : List α
⊢ ((fun n ↦ replicate n default) u.length).length = u.length

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : Fin n), f ↑x = f ↑((equivSubtype.trans (Equiv.subtypeEquivRight ⋯)) x)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
⊢ ¬univ.Countable ↔ Uncountable α

Tactic:
countable_univ_iff,

Goal state after:
α : Type u
⊢ ¬Countable α ↔ Uncountable α
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (f '' s).Countable

Tactic:
rw [image_eq_range]
  have := hs.to_subtype
  apply countable_range

Goal state after:
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u2} ↑t
⊢ Small.{u, u3} ↑(Set.image2 f s t)

Tactic:
by
  rw [← Set.image_uncurry_prod]
  infer_instance

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ {x | ¬p x} ↔ ¬p x

Tactic:
by simp

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 : ℕ
β : Type u_6
γ : Type u_7
v : Vector α n
i : Fin n
a : α
⊢ ((↑v).set (↑i) a).length = n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
⊢ (v.set i a).get j = if i = j then a else v.get j

Tactic:
split_ifs <;> (try simp [*]); rwa [get_set_of_ne]

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ (sumLexIioIci x).symm y = toLex (Sum.inl ⟨y, h⟩)

Tactic:
symm_apply_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ y = (sumLexIioIci x) (toLex (Sum.inl ⟨y, h⟩))
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ (sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
symm_apply_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ y = (sumLexIioIci x) (toLex (Sum.inr ⟨y, h⟩))
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ (sumLexIicIoi x).symm y = toLex (Sum.inl ⟨y, h⟩)

Tactic:
symm_apply_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ y = (sumLexIicIoi x) (toLex (Sum.inl ⟨y, h⟩))