mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
⊢ (if p a then {a} else 0).bind f = if p a then f a else 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
a✝ : M
l : List M
a : M
h : a ∈ ⟦l⟧
⊢ a ∣ prod ⟦l⟧

Tactic:
simpa using List.dvd_prod h

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ ∀ i ∈ s, ∀ i_1 ∈ s, Disjoint (f i) (g i_1)

Tactic:
intros i hi j hj

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hj : j ∈ s
⊢ Disjoint (f i) (g j)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations = (zipWith (fun x1 x2 ↦ x1 ++ x2) l.tails l.inits).dropLast

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h

Goal state after:
α : Type u
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ (hd :: tl).cyclicPermutations = (zipWith (fun x1 x2 ↦ x1 ++ x2) (hd :: tl).tails (hd :: tl).inits).dropLast
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.offDiag.length = l.length ^ 2 - l.length

Tactic:
simp [length_offDiag', Nat.mul_sub, Nat.pow_two]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
descFactorial_eq_zero_iff_lt.2 h,

Goal state after:
case inl
n k : ℕ
h : n < k
⊢ 0 = k ! * n.choose k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k < n
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
grind [k.choose_mono hk]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)

pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
· refine fun k hk ↦ Fintype.card_congr ?_
    rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
⊢ y ∈ v i → y ∈ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
y_in

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)

Tactic:
ext
  simp only [Set.mem_iUnion, Set.sUnion_image]
  grind

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
z : M
hz : z ∈ s
⊢ motive x z hx ⋯

Tactic:
induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
j : ι
hb : b ∈ S j
⊢ a * b = b * a

Tactic:
obtain ⟨k, hik, hjk⟩ := dir i j

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
simp_rw [mem_closure_singleton, exists_exists_eq_and]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
by
  simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Subsemigroup.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
by
    have : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m := by
      rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp
    simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : { g // f.ker ≤ g.ker }
⊢ (fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g) = g

Tactic:
ext
    simp only [comp_apply, liftOfRightInverseAux_comp_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
⊢ a * b = b * a

Tactic:
obtain ⟨k, hik, hjk⟩ := dir i j

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case mul_right
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x✝ : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
x : M
hx✝ : x ∈ closure s
y : M
hy : y ∈ s
ih : motive x
⊢ motive (x * y)

Tactic:
| mul_right x _ y hy ih =>

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    ((if r hd val✝ then some hd else some val✝) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
simp_rw [mem_closure_singleton, exists_exists_eq_and]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n) ∧ m ∈ s

Tactic:
by
          simp only [h.2, and_true]
          exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))

Goal state after:
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (hd' :: tl', tail)

Tactic:
right

Goal state after:
case mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ #(powersetCard n s) = 0

Tactic:
by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id ⊆ u

Tactic:
simp_rw [Finset.sup_le_iff, mem_powersetCard]
    rintro x ⟨h, -⟩
    exact h

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i ∈ s, i = sInf s

Tactic:
by
  rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']
  · convert! h
    rw [← sInf_range, Subtype.range_coe]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}

Tactic:
exact h.le_and_le_iff

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case inr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ≤ b ∧ b ≤ a
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
· inhabit ι
    exact ⟨default, fun j hj ↦ ⟨h.left j, h.right j⟩⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑a ⋖ ⊤ ↔ IsMax a

Tactic:
by
  simp [covBy_iff_Ioo_eq, ← image_coe_Ioi]

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = s.sup (f ∘ invFunOn f (f ⁻¹' ↑s))

Tactic:
← sup_image

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = (image (invFunOn f (f ⁻¹' ↑s)) s).sup f
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b

Tactic:
obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
  exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ⊢ 0 ∈ ∅ ∨ ∅ = ∅

Tactic:
right

Goal state after:
⊢ ∅ = ∅
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅

Tactic:
right

Goal state after:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

Tactic:
rw [add_mod_right] at hkl
      refine (hln <| ih hl ?_ hkl.symm).elim
      simpa using Nat.lt_add_of_pos_right (n := n) ha

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
exact h.exists_monotone_subseq f

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), ↑(f (g n)) ∈ s
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

pp: case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
· rcases hs.exists_lt hgs with ⟨m, n, hlt, hr⟩
    exact ⟨g m, g n, g.strictMono hlt, hr⟩

Goal state after:
case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case inl
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ ∅.Finite ↔ BddBelow ∅ ∧ BddAbove ∅

Tactic:
simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #∅ = #∅ - 1

Tactic:
card_empty,

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ 0 = 0 - 1
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #∅ = #∅ - 1

Tactic:
card_empty,

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ 0 = 0 - 1
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iic a) - 1

Tactic:
Iic_eq_cons_Iio,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(cons a (Iio a) ⋯) - 1
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ a ∈ orbit G (g • a)

Tactic:
simp only [orbit_smul, mem_orbit_self]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⩿ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S T : Set M
inst✝ : Mul M
⊢ (S ∪ T).centralizer = S.centralizer ∩ T.centralizer

Tactic:
simp [centralizer, or_imp, forall_and, ofPred_and]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
z : M
a : z ∈ center M
g : M
⊢ g * z = z * g

Tactic:
rw [IsMulCentral.comm a g]

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
y : α
hy : y ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
⊢ x ≠ y → Commute x y

Tactic:
simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ≠ y → Commute x y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

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

Tactic:
simp only [prod_ite_irrel, prod_const_one]

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

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

Tactic:
simp only [prod_ite_irrel, prod_const_one]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ ⇑(iInf f) = ⨅ i, ⇑(f i)

Tactic:
rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
x✝ y : M
h : c x✝ y
x : M
⊢ c (x⁻¹ * x) 1

Tactic:
simp only [inv_mul_cancel, c.refl 1]

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

Goal state before:
pp: α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ [] ++ tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴) = (x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴) L₅

Tactic:
right

Goal state after:
α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ ∃ L₅, Step ([] ++ tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ (x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴ = [] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴) ∨
    ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴) L₅ ∧ Step ([] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴)) L₅

Tactic:
right

Goal state after:
α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴) L₅ ∧ Step ([] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴)) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case false
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, false) :: (x✝, !false) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

Tactic:
simp [Lift.aux, List.prod_append]

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

Goal state before:
pp: case true
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, true) :: (x✝, !true) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

Tactic:
simp [Lift.aux, List.prod_append]

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

Goal state before:
pp: case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁) * Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₂)

Tactic:
simp [Lift.aux, List.prod_append]

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

Goal state before:
pp: case a
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
x : ι
h : x ∈ s
a✝ : ⟨x, h⟩ ∈ univ
⊢ f ↑⟨x, h⟩ = g ⟨x, h⟩

Tactic:
exact w x h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ Nontrivial (G ⧸ N) ↔ N ≠ ⊤

Tactic:
by
  simp [← not_subsingleton_iff_nontrivial]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

Tactic:
Subgroup.closure_le,

Goal state after:
case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
G' : Type u_5
inst✝ : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
by
  rw [fg_iff_submonoid_fg] at *
  exact hP.prod hQ

Goal state after: