mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (Multiset.map f (a ::ₘ s.val)).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯

Tactic:
Multiset.map_cons,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (f a ::ₘ Multiset.map f s.val).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (Multiset.map f (a ::ₘ s.val)).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a

Tactic:
Multiset.map_cons,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (f a ::ₘ Multiset.map f s.val).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
a✝ : j ∈ insert i (univ.erase i)
⊢ (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M j) (x j)) = Pi.mulSingle j (x j) i

Tactic:
dsimp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
⊢ (fun x1 x2 ↦ x1 = x2) ≤ ⇑(r.map f)

Tactic:
by rintro _ _ rfl; exact .refl _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot ⇑r
w : α
⊢ (fun x ↦ x.liftOn' (fun w ↦ Quotient.mk'' (Quotient.mk'' w)) ⋯)
      ((fun x ↦ x.liftOn' (fun w ↦ Quotient.liftOn' w Quotient.mk'' ⋯) ⋯) (Quotient.mk'' (Quotient.mk'' w))) =
    Quotient.mk'' (Quotient.mk'' w)

Tactic:
change ⟦_⟧ = _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot ⇑r
w : α
⊢ ⟦Quotient.mk'' w⟧ = Quotient.mk'' (Quotient.mk'' w)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ (fun x ↦ x.liftOn' (fun w ↦ Quotient.liftOn' w Quotient.mk'' ⋯) ⋯)
      ((fun x ↦ x.liftOn' (fun w ↦ Quotient.mk'' (Quotient.mk'' w)) ⋯) (Quotient.mk'' y)) =
    Quotient.mk'' y

Tactic:
change ⟦_⟧ = _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ ⟦y⟧ = Quotient.mk'' y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c.toSetoid = ⊤ ↔ c = ⊤

Tactic:
by rw [← toSetoid_top, toSetoid_inj]

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

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : f.comp c.mk' = g.comp c.mk'
⊢ f = g

Tactic:
rw [← lift_apply_mk' f, ← lift_apply_mk' g]

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : f.comp c.mk' = g.comp c.mk'
⊢ c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
dsimp

Goal state after:
case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: (tl ++ L2)) < sizeOf (hd :: (tl ++ (x, b) :: (x, !b) :: L2))
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1 ∈ N, x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N

Tactic:
simpa using hz

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ ∀ (x : ↥N), (fun x_1 ↦ x_1 * ↑x⁻¹) '' s = (fun x_1 ↦ x_1 * ↑x) ⁻¹' s

Tactic:
exact fun x ↦ image_mul_right'

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ { toSetoid := leftRel f.ker, mul' := ⋯ } x✝ y✝ ↔ (Con.ker f) x✝ y✝

Tactic:
Con.rel_mk,

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ (leftRel f.ker) x✝ y✝ ↔ (Con.ker f) x✝ y✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
hm : ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k
⊢ ∏ k ∈ range (N + (m + 1)), u k = ∏ k ∈ range N, u k

Tactic:
simp [← add_assoc, prod_range_succ, hm, hu]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ { toSetoid := leftRel c.subgroup, mul' := ⋯ } x y ↔ c x y

Tactic:
Con.rel_mk,

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ (leftRel c.subgroup) x y ↔ c x y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
refine prod_subset hs fun x _ hx => ?_

Goal state after:
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
x✝ : x ∈ s
hx : x ∉ m.toFinset
⊢ x ^ count x m = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
⊢ Function.Injective of

Tactic:
exact fun x y hoxy ↦ Classical.by_contradiction fun hxy : x ≠ y ↦
    let f : FreeAbelianGroup α →+ ℤ := lift fun z ↦ if x = z then (1 : ℤ) else 0
    have hfx1 : f (of x) = 1 := (lift_apply_of _ _).trans <| if_pos rfl
    have hfy1 : f (of y) = 1 := hoxy ▸ hfx1
    have hfy0 : f (of y) = 0 := (lift_apply_of _ _).trans <| if_neg hxy
    one_ne_zero <| hfy1.symm.trans hfy0

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
x : α
a✝ : (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)
⊢ (lift (f + g)) (-of x) = (lift f) (-of x) + (lift g) (-of x)

Tactic:
| neg x =>

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = m.card

Tactic:
rw [← toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]
  congr with a
  simpa using hms a

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

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
· rw [prod_le_iff]
    constructor <;>
      · rw [map_commutator]
        apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ ∀ {x y : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) → ∃ u v, u • x.fst = v • y.fst ∧ ↑u * ↑x.snd = v * ↑y.snd

Tactic:
rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨u, v, hru, hsu⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • (r', s').fst = v • (r, s).fst
hsu : ↑u * ↑(r', s').snd = v * ↑(r, s).snd
⊢ ∃ u v, u • (r, s).fst = v • (r', s').fst ∧ ↑u * ↑(r, s).snd = v * ↑(r', s').snd
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 → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₂ : ↑u * ↑(r₂, s₂).snd = v * ↑(r₁, s₁).snd
⊢ P (r₁, s₁).fst (r₁, s₁).snd = P (r₂, s₂).fst (r₂, s₂).snd

Tactic:
dsimp at *

Goal state after:
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 → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
⊢ P r₁ s₁ = P r₂ s₂
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • mk a b = mk (c • a) b

Tactic:
by
  rw [mk, mk, ← OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv]
  change (c • 1) • a /ₒ (b * 1) = _
  rw [smul_assoc, one_smul, mul_one]

Goal state after:
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
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a b : WithZero αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun a ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ a ≤ b

Tactic:
by
    cases a <;> cases b <;>
    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
f : S.LocalizationMap N
z : N
⊢ f ↑(f.sec z).2 * z = f.toMonoidHom ↑(f.sec z).2 * z

Tactic:
dsimp

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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f ↑y * f x = f.toMonoidHom ↑y * f x

Tactic:
dsimp

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)
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
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom ↑x.2 = f.toMonoidHom x.1

Tactic:
dsimp

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
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f ↑x.2 = f x.1
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
y : ↥S
⊢ f ↑y = f.toMonoidHom ↑y

Tactic:
dsimp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk x y * (monoidOf S).toMonoidHom ↑y = (monoidOf S) x

Tactic:
dsimp

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk x y * (monoidOf S) ↑y = (monoidOf S) x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ pred^[k] (pred^[1] b) = a

Tactic:
iterate_one,

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ pred^[k] (pred b) = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
⊢ Ioo a b = ∅

Tactic:
· ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
⊢ (if h : pred ↑⟨x, hx⟩ ∈ s then ⟨pred ↑⟨x, hx⟩, h⟩ else ⟨x, hx⟩) ≤ ⟨x, hx⟩

Tactic:
dsimp

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
⊢ (if h : pred x ∈ s then ⟨pred x, h⟩ else ⟨x, hx⟩) ≤ ⟨x, hx⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inl
c : ℕ∞
hc : c ≠ 0
⊢ ⊤ ≤ ⊤ * c

Tactic:
simp [top_mul hc]

Goal state after:
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)
⊢ (↑s).piecewise f g = s.piecewise f g

Tactic:
by
  ext
  congr

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
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < n

Tactic:
exact i.2

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨↑⟨i, ih⟩ + 1, ⋯⟩

Tactic:
dsimp

Goal state after:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨i + 1, ⋯⟩
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x, f x = f a * f b

Tactic:
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx <;>
    exact fun hc => (hc (Finset.mem_univ _)).elim

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

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

Tactic:
dsimp

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #(image List.ofFn univ) = Fintype.card α ^ s

Tactic:
by
          simp [card_image_of_injective univ List.ofFn_injective]

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i + 1, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.castPred ⋯)) a

Tactic:
dsimp

Goal state after:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx (i + 1) =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (Vector.traverse f (x✝ ::ᵥ w✝)) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) (x✝ ::ᵥ w✝)

Tactic:
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
    rfl

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact (not_inl_lt_inr ha).elim

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

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x

Tactic:
rw [ciSup_le_iff' H]

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ∀ (i : ↑(Iio x)), succ ↑i ≤ x
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b < f a
c : α
hc : f c = b
⊢ c < a

Tactic:
rwa [← hc, f.lt_iff_lt] at h

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (fun o ↦ o.toOption) ↑o = (↑o).toOption

Tactic:
dsimp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (↑o).toOption = (↑o).toOption
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part α✝
y : Part β✝
⊢ (x <* y).Dom ↔ (const β✝ <$> x <*> y).Dom

Tactic:
by simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, (· <$> ·), and_comm]

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ c_1 ⊆ {s | c ⊆ s ∧ IsChain r s},
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c_1 → c_1.Nonempty → ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ c_1, s ⊆ ub

Tactic:
rintro cs hcs₀ hcs₁ ⟨s, hs⟩

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ cs, s ⊆ ub
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
⊢ c i ≤ Part.ωSup c

Tactic:
by
    intro x hx
    rw [← eq_some_iff] at hx ⊢
    rw [ωSup_eq_some]
    rw [← hx]
    exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))
      i ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
dsimp

Goal state after:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ (f (c i)) (ωSup (c.map { toFun := g, monotone' := ⋯ })) ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 ↦ x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 ↦ x1 < x2) j
this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))
⊢ c ≤ j

Tactic:
simpa only [mk_out] using this

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : a < b
⊢ a + 1 ≤ b

Tactic:
induction a, b using Cardinal.inductionOn₂ with | mk α β
  obtain ⟨f⟩ := h.le
  have hf : ¬Surjective f := fun hn ↦ h.not_ge (mk_le_of_surjective hn)
  rw [Surjective, not_forall] at hf
  obtain ⟨b, hb⟩ := hf
  rw [← mk_option]
  exact (f.optionElim b hb).cardinal_le

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

Goal state before:
pp: α : Type u
⊢ ∃ x, WellFoundedLT α

Tactic:
by
  classical
  exact ⟨linearOrderOfSTO WellOrderingRel, ⟨WellOrderingRel.isWellOrder.wf⟩⟩

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
i : ι
⊢ ¬∀ (x : Quotient.out (g i)), ∃ x_1, G ⟨i, x_1⟩ i = x

Tactic:
refine fun h => (H i).not_ge ?_

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, G ⟨i, x_1⟩ i = x
⊢ g i ≤ f i
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{max u v, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)

Tactic:
rw [lift_umax.{v, u}]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ succ ↑n = ↑n + 1

Tactic:
refine (succ_le_of_lt ?_).antisymm (add_one_le_of_lt <| lt_succ _)

Goal state after:
n : ℕ
⊢ ↑n < ↑n + 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = sum fun i ↦ lift.{v, u} #↑(f i)

Tactic:
← lift_sum,

Goal state after:
α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = lift.{v, max u v} (sum fun i ↦ #↑(f i))
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ (↑e).toFun = ⇑e

Tactic:
dsimp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: F : Type u_16
M : Type u_17
N : Type u_18
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
c : ℤˣ
m : M
⊢ f (c • m) = c • f m

Tactic:
by
  simp [Units.smul_def]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn • (a + a') = mn • a + mn • a'

Tactic:
change mn.1 • mn.2 • _ = (_ : α); rw [smul_add, smul_add]; rfl

Goal state after: