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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

Tactic:
by
  rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
c : ↑(Icc a b)
hc : c ∈ S
⊢ sInf (Subtype.val '' S) ≤ b

Tactic:
exact le_trans (csInf_le ⟨a, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.1⟩ ⟨c, hc, rfl⟩) c.2.2

Goal state after:
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
by
  rw [mul_invOf_eq_iff_eq_mul_right, ← Int.commute_cast, mul_assoc,
    ← mul_left_eq_iff_eq_invOf_mul, Int.commute_cast]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
← subset_compl_iff_disjoint_right,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ mulSupport f ⊆ sᶜ ↔ EqOn f 1 s
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ ¬0 < 0

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ |x - ↑z|

Tactic:
rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]
    conv_rhs => rw [← fract_add_floor x]
    rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_comm]
    norm_cast
    rwa [le_sub_one_iff, floor_lt]

Goal state after:
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' k : ℕ
h1 : CSLiftVal n n'
⊢ n' ^ k = CSLift.lift (n ^ k)

Tactic:
by simp [h1.1, CSLift.lift]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
⊢ Monotone fun n ↦ a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ 0 - 1 < a

Tactic:
zero_sub

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ -1 < a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌈a⌉ < ⌈a⌉ + 1

Tactic:
apply lt_add_one

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
rw [this, ← self_sub_fract]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - (a - fract a + 1)
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
x y : B
⊢ f (c • (x * y)) = f (c • x * c • y)

Tactic:
by simp only [smul, f.map_mul, smul_mul']

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
⊢ ∃ z, x < ↑z / ↑n ∧ ↑z / ↑n < y

Tactic:
obtain ⟨z, zh⟩ := exists_floor (x * n)

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
⊢ ∃ z, x < ↑z / ↑n ∧ ↑z / ↑n < y
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
⊢ ∀ {s₂ : Multiset α} {e : ↑l₁ = s₂} {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H =
      ↑(List.pmap f l₁ H₁)

Tactic:
intro s₂ e _

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
H✝ : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H✝ =
    ↑(List.pmap f l₁ H₁)
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
rw [replicate_succ]

Goal state after:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
intro h
    rw [replicate_succ]
    exact ⟨x, cons_le_cons _ h⟩

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (some '' {x | x ∈ l})

Tactic:
rw [← range_list_get, ← range_comp]

Goal state after:
α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (range (some ∘ l.get))
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.foldl List.erase l₁ l₂) = foldl erase ↑l₁ ↑l₂

Tactic:
symm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase ↑l₁ ↑l₂ = ↑(List.foldl List.erase l₁ l₂)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys.dedup = ys.dedup

Tactic:
Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ ys.dedup = ys.dedup
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndunion t = t

Tactic:
by
  induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.union_eq_right h

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Tactic:
rw [inter_comm, insert_inter_of_mem h, inter_comm]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.attach = ∅ ↔ s = ∅

Tactic:
by
  simp [eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s.toFinset.Nonempty ↔ s ≠ 0

Tactic:
simp only [toFinset_eq_empty, Ne, Finset.nonempty_iff_ne_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ image f s₁ ⊆ image f s₂

Tactic:
by
  simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]

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

Goal state before:
pp: n : ℕ
⊢ Injective predAbove

Tactic:
intro i j hij
  obtain ⟨n, rfl⟩ := Nat.exists_add_one_eq.2 i.size_positive
  wlog! h : i < j generalizing i j
  · obtain h | rfl := h.lt_or_eq
    · exact (this hij.symm h).symm
    · rfl
  replace hij := congr_fun hij i.succ
  rw [predAbove_succ_self, Fin.predAbove_of_le_castSucc _ _ (by simpa),
    ← Fin.castSucc_inj, castSucc_castPred] at hij
  exact (i.castSucc_lt_succ.ne hij).elim

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ ↑0 ≠ ↑((j - i).castLT ⋯)

Tactic:
simp [coe_sub_iff_le.mpr (Fin.le_of_lt hij)]

Goal state after:
n : ℕ
i j : Fin n
hij : i < j
⊢ ¬0 = ↑j - ↑i
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup ↔ Function.Injective f

Tactic:
by
  refine ⟨?_, nodup_ofFn_ofInjective⟩
  refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f
  · intro _
    exact Function.injective_of_subsingleton _
  · intro h
    rw [Fin.cons_injective_iff]
    simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
    exact h.imp_right ih

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

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ univ = {x}

Tactic:
symm

Goal state after:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: n : ℕ
s : Finset (Fin n)
⊢ #s ≤ n

Tactic:
simpa only [Fintype.card_fin] using s.card_le_univ

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

Goal state before:
pp: case mp.cons_cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
obtain ⟨f, hf⟩ := IH
      refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
      · rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
      · rintro ⟨_ | i⟩
        · simp
        · simpa using hf _

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ ∀ (a b : α), (decide (r a b) || decide (r b a)) = true

Tactic:
simpa using total_of r

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun j ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)

Tactic:
exact Fin.find_min hⱼ hi

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha✝ : a ∈ l
ha : a ∈ l.dropLast ∨ a = l.getLast ⋯
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = countP p as

Tactic:
refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℤ
h : l.prod = -1
⊢ -1 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 * -1 = 1

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (bind 0 fun x ↦ {f x}) = map f 0

Tactic:
by rw [zero_bind, map_zero]

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

Goal state before:
pp: α : Type u_1
l : List α
x : α × α
⊢ x ∈ l.offDiag ↔ ∃ i x_1 j x_2, i ≠ j ∧ l[i] = x.fst ∧ l[j] = x.snd

Tactic:
by
  rcases x with ⟨x, y⟩
  simp only [offDiag, exists_mem_zipIdx, mem_eraseIdx_iff_getElem, mem_flatMap, mem_map,
    Nat.zero_add, Prod.ext_iff, ← exists_and_right, exists_and_left, @exists_comm α, and_assoc,
    exists_eq_left', ne_comm]

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

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0

Tactic:
decide

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

Goal state before:
pp: ⊢ (0 + 1) * choose 0 0 = (0 + 1).choose (0 + 1) * (0 + 1)

Tactic:
decide

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ FactorsThrough f s.domRestrict ↔ ∃ g, f = g ∘ s.domRestrict

Tactic:
factorsThrough_iff

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∃ e, f = e ∘ s.domRestrict) ↔ ∃ g, f = g ∘ s.domRestrict
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Tactic:
calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = f 0 ∪ iUnion (f ∘ Fin.succ)

Tactic:
cases f using Fin.consCases

Goal state after:
case cons
α : Type u_1
n : ℕ
x₀✝ : Set α
x✝ : Fin n → Set α
⊢ ⋃ i, Fin.cons x₀✝ x✝ i = Fin.cons x₀✝ x✝ 0 ∪ iUnion (Fin.cons x₀✝ x✝ ∘ Fin.succ)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ Quotient.lift conjugatesOf ⋯ (ConjClasses.mk b) ↔ IsConj b a

Tactic:
← quotient_mk_eq_mk,

Goal state after:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ Quotient.lift conjugatesOf ⋯ ⟦b⟧ ↔ IsConj b a
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ f 1 = g 1

Tactic:
f.map_one,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 = g 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
n : ℕ
⊢ {a} ^ (n + 1) = {a ^ (n + 1)}

Tactic:
by simp [pow_succ, singleton_pow _ n]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
have hst : (s * t).Nonempty := h.symm.subst one_nonempty
    obtain ⟨a, ha⟩ := hst.of_image2_left
    obtain ⟨b, hb⟩ := hst.of_image2_right
    have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb
    refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
    · exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
    · exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
rw [div_eq_mul_inv]

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑H ∩ Set.range ⇑f = ↑(f.range ⊓ H)

Tactic:
coe_inf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑H ∩ Set.range ⇑f = ↑f.range ∩ ↑H
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : H ⊔ f.ker = K ⊔ f.ker
⊢ H = K

Tactic:
sup_of_le_left hH,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : H = K ⊔ f.ker
⊢ H = K
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 0 < 2

Tactic:
decide

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

Goal state before:
pp: A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))

Tactic:
symm

Goal state after:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * (b * b) = a * b

Tactic:
hb.eq

Goal state after:
S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * b = a * b
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

pp: case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid

Tactic:
· suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
    exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)

Goal state after:
case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
· specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Tactic:
eq_top_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr max 0 (map f tl)
⊢ f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))

Tactic:
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
    exact (hadd _ _).trans (max_le_max le_rfl IH)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f l.prod ≤ (map f l).sum

Tactic:
induction l with
  | nil => simp [h_one]
  | cons hd tl IH => grw [prod_cons, h_mul, IH]; simp

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))

Tactic:
symm

Goal state after:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)

Tactic:
exact ofMul_image_powers_eq_multiples_ofMul

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
· rw [h] at hm
      simp_all

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Tactic:
simp_rw [disjSum, mem_add, mem_map]

Goal state after: