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

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddAbove t
h : sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) = ↑(sSup t)

Tactic:
by simp [h, h', h'']

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddBelow t
h : sInf (Subtype.val '' t) ∈ s
⊢ sInf (Subtype.val '' t) = ↑(sInf t)

Tactic:
by simp [h, h', h'']

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

Tactic:
← NNRat.cast_ofScientific (K := K),

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ ↑(OfScientific.ofScientific m s e) = ↑(OfScientific.ofScientific m s e)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊↑n * a⌋ / n = ⌊a⌋

Tactic:
rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]

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

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Tactic:
· rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
      simp [hl]

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 b : R
⊢ ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

Tactic:
rw [ceil_le, Int.cast_add]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b ≤ ↑⌈a⌉ + ↑⌈b⌉
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid G
inst✝³ : LinearOrder G
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
f : G →* M
hf : StrictMono ⇑f
x x✝ : G
h : 1 < x✝
⊢ ∀ (a : ℕ), f x ≤ f x✝ ^ a → x ≤ x✝ ^ a

Tactic:
simp [← map_pow, hf.le_iff_le]

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * (↑⌊a⌋ + 1) ≤ ↑⌊a⌋

Tactic:
_root_.mul_add_one,

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * ↑⌊a⌋ + b ≤ ↑⌊a⌋
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨Nat.find this, h.trans_le ?_, Nat.find_spec this⟩

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
⊢ b * c ≤ c ^ Nat.find this
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
hy : R (f (l + n • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)

Tactic:
← Int.add_one_le_iff,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 + 1 ≤ n
hy : R (f (l + n • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K✝ : Type u_4
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ Archimedean K

Tactic:
rw [archimedean_iff_int_le]
  exact fun x => ⟨⌈x⌉, Int.le_ceil x⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 1 ≤ count a s ↔ a ∈ s

Tactic:
by
  rw [succ_le_iff, count_pos]

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

Goal state before:
pp: case mp.cons
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
| @cons a' b as' bs ha'b h ih =>

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
a : α
as' : Multiset α
⊢ flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
rw [rel_flip, flip]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+ l₂
hne : l₂ ≠ []
hl : l₂.head hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
by
  grind [List.IsSuffix]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ Surjective (map f)

Tactic:
intro s
  induction s using Multiset.induction_on with
  | empty => exact ⟨0, map_zero _⟩
  | cons x s ih =>
    obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ (map val s.attach).erase ↑x = s.erase ↑x

Tactic:
attach_map_val

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ s.erase ↑x = s.erase ↑x
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t + s ∩ t = s

Tactic:
rw [inter_comm]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t + t ∩ s = s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint {a} l ↔ ¬a ∈ l

Tactic:
singleton_disjoint

Goal state after:
α : Type u_1
l : Multiset α
a : α
⊢ ¬a ∈ l ↔ ¬a ∈ l
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint {a} t ∧ _root_.Disjoint s t ↔ ¬a ∈ t ∧ _root_.Disjoint s t

Tactic:
singleton_disjoint

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ ¬a ∈ t ∧ _root_.Disjoint s t ↔ ¬a ∈ t ∧ _root_.Disjoint s t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂

Tactic:
apply take_prefix

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

Goal state before:
pp: α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] ↔ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

Tactic:
constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · simp

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ (a :: s.toList).Nodup

Tactic:
simp [h, nodup_toList s]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

Tactic:
by
  constructor <;> simp +contextual [disjoint_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset α
⊢ (↑s).toFinset = s

Tactic:
convert! Finset.toFinset_coe s

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

Goal state before:
pp: m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h : m = n
⊢ Fin.cast h ⊤ = ⊤

Tactic:
by
  simp [← val_inj, h]

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

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ Injective (cons x₀ x)

Tactic:
by
  intro i j
  cases i using Fin.cases <;> cases j using Fin.cases <;> aesop (add simp [hx.eq_iff])

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

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}

pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2

Tactic:
· rw [card_eq_succ]
    grind [card_eq_one]

Goal state after:
case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (succAbove p i)

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

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ snoc f a i.rev = cons a (f ∘ rev) i

Tactic:
simpa using insertNth_rev (last n) a f i

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedGE ↔ Pairwise (fun x1 x2 ↦ x1 ≥ x2) l

Tactic:
simp only [sortedGE_iff_antitone_get, antitone_iff_forall_lt, Fin.forall_iff]

Goal state after:
α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i_1, h_1⟩ ≤ l.get ⟨i, h⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 ≥ x2) l
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedLE ↔ l.SortedGE

Tactic:
grind [OrderDual.toDual_le_toDual]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedGE ↔ l.SortedLE

Tactic:
grind [OrderDual.toDual_le_toDual]

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (find? fun x ↦ decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none

Tactic:
by
  simp_rw [find?_eq_dite, decide_eq_true_eq]

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x * xs.prod) = ((map op xs).reverse.concat (op x)).prod

Tactic:
List.prod_concat,

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x * xs.prod) = (map op xs).reverse.prod * op x
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun i ↦ fold op (b i) (t i)) (a ::ₘ ha))

Tactic:
cons_bind,

Goal state after:
case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) (a ::ₘ ha))
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
· apply congr_arg
    grind

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: case mk
α : Type u_1
x : α × α
val✝ : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
⊢ x ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }.offDiag ↔
    x.1 ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs } ∧
      x.2 ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs } ∧ x.1 ≠ x.2

Tactic:
exact hs.mem_offDiag

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.diag.Nonempty ↔ s.Nonempty

Tactic:
simp [diag]

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

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

Tactic:
simp [diag]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.diag = #s

Tactic:
simp [diag]

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

Goal state before:
pp: α : Type u_1
x✝¹ x✝ : Finset α
⊢ x✝¹ ⊆ x✝ → x✝¹.diag ⊆ x✝.diag

Tactic:
simp [diag]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Subsemigroup M
h : i ∈ s
⊢ a✝ ∈ i

Tactic:
apply Set.mem_iInter₂.1 hx i h

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Submonoid M
h : i ∈ s
⊢ a✝ ∈ i

Tactic:
apply Set.mem_iInter₂.1 hx i h

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : a ∈ Set.ofPred IsUnit
hb : b ∈ Set.ofPred IsUnit
⊢ a * b ∈ Set.ofPred IsUnit

Tactic:
Set.mem_ofPred_eq

Goal state after:
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ Set.ofPred IsUnit ↔ IsUnit a

Tactic:
Set.mem_ofPred_eq

Goal state after:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ IsUnit a ↔ IsUnit a
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
s : Set (Subgroup G)
x : G
hx : x ∈ ((⨅ S ∈ s, S.toSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯).carrier
i : Subgroup G
h : i ∈ s
⊢ x ∈ i

Tactic:
apply Set.mem_iInter₂.1 hx i h

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ map f ⊥ = ⊥

Tactic:
map_bot

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ map f ⊥ = ⊥

Tactic:
map_bot

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (inr M N) x2 ∈ u

Tactic:
apply hK

Goal state after:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (inr M N) x2 ∈ map (inr M N) t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ ↑(mrange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_mrange, coe_top]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
by
  apply forall_congr'; intro H
  simp only [lt_iff_le_and_ne, le_normalizer, Ne]
  tauto

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
Set.smul_set_inter,

Goal state after:
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s) ∩ z • (t⁻¹ * t)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1
h₂ : ∃ i_1, i_1 ∈ i :: l ∧ f i_1 < g i_1
⊢ (map f (i :: l)).prod < (map g (i :: l)).prod

Tactic:
simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
    simp only [mem_cons, exists_eq_or_imp] at h₂
    cases h₂
    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
    · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : ∃ i, p i
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
by
  rw [← nonempty_subtype] at hp
  rw [iSup_subtype', mem_iSup_of_directed]
  · simp
  rw [← Function.comp_def, directed_comp]
  exact hS.directed_val

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

Goal state before:
pp: case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b

Tactic:
obtain ⟨i, a⟩ := a
    dsimp only
    rintro (h | ⟨rfl, h⟩)
    · exact Lex.left _ _ h
    · exact Lex.right _ h

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]
  exact le_sup_right

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ y ∈ l, y ∈ s
h2 : l.prod = x
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : M
h : x ∈ closure s
⊢ motive x h

Tactic:
closure_eq_mrange

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : M
h✝ : x ∈ closure s
h : x ∈ mrange (FreeMonoid.lift Subtype.val)
⊢ motive x h✝
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : x ∈ closure s
m : Mᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
rwa [← op_closure] at hm

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * m.succ) = (x ^ k) ^ (m + 1)

Tactic:
pow_mul

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ k) ^ m.succ = (x ^ k) ^ (m + 1)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ ((x ^ (m + 1)) ^ (n - 1)) ^ k = (x ^ m.succ) ^ ((n - 1) * k)

Tactic:
pow_mul

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ ((x ^ (m + 1)) ^ (n - 1)) ^ k = ((x ^ m.succ) ^ (n - 1)) ^ k
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: case cons
α : Type u_2
inst✝ : DecidableEq α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
h : s✝.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ s✝ → a.Nodup
⊢ (a✝ ::ₘ s✝).sup.Nodup ↔ ∀ (a : Multiset α), a ∈ a✝ ::ₘ s✝ → a.Nodup

Tactic:
| cons _ _ h =>

Goal state after: