mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
rw [extend_apply' _ _ _ hf]

Goal state after:
case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ

Tactic:
exact div_le_div'' h.1 h.2

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

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!

Tactic:
rw [Nat.sub_one, factorial_mul_ascFactorial]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ ⌊f a + 1 / 2⌋ = ⌊a + 1 / 2⌋

Tactic:
← map_floor _ hf,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ ⌊f a + 1 / 2⌋ = ⌊f (a + 1 / 2)⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1 ∈ s, fract x_1 = x

Tactic:
rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩
    obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩
    exact ⟨y, hys, rfl⟩

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ f a - ↑⌊f a⌋ = f (a - ↑⌊a⌋)

Tactic:
map_sub,

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ f a - ↑⌊f a⌋ = f a - f ↑⌊a⌋
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
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
⊢ ¬y ≤ (↑0 * δ) ^ n

Tactic:
by simpa [zero_pow hn] using hy

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

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

Tactic:
count_pos

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s ↔ a ∈ s
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mk.cons
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
head✝ : α
tail✝ : List α
ih : p (Quot.mk (⇑(isSetoid α)) tail✝)
⊢ p (Quot.mk (⇑(isSetoid α)) (head✝ :: tail✝))

Tactic:
exact cons _ _ ih

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
⊢ map f (s.erase x) = (map f s).erase (f x)

Tactic:
induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_

Goal state after:
case cons
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
x : α
h : x ∈ s
⊢ map f (s.erase x) = (map f s).erase (f x)

Tactic:
induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_

Goal state after:
case cons
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
xs : List α
⊢ (map f xs).dedup = map f xs.dedup

Tactic:
by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [map_cons]
    by_cases h : x ∈ xs
    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
    · rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂

Tactic:
by
  simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]
  rfl

Goal state after:
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]
  revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  by_cases h : a ∈ s
  · rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
  · rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s - filter p s = filter (fun a ↦ ¬p a) s

Tactic:
ext a; by_cases h : p a <;> simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Unique α
s : Finset α
⊢ s.Nonempty ↔ s = {default}

Tactic:
by
  simp [eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
val_eq_singleton_iff

Goal state after:
α : Type u_1
a : α
s : Finset α
⊢ s = {a} ↔ s = {a}
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq γ
g : β → γ
s : Finset α
a✝ : γ
⊢ a✝ ∈ (image g ∘ image f) s ↔ a✝ ∈ image (g ∘ f) s

Tactic:
simp [image_image]

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

Goal state before:
pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
· rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]

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

Goal state before:
pp: case zero
k : Fin (Nat.succ 0)
this : NeZero (Nat.succ 0)
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
simp only [Fin.isValue, Fin.zero_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : α → β
hi : Set.MapsTo i ↑s ↑t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ ∀ b ∈ t, ∃ a, ∃ (_ : a ∈ s), i a = b

Tactic:
simpa using! i_surj

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ i.castPred hi = j

Tactic:
by simp_rw [h, castPred_castSucc]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b < a.succ.castPred ha ↔ b ≤ a

Tactic:
lt_castPred_iff,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b.castSucc < a.succ ↔ b ≤ a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
⊢ a.pred ha < b.castPred hb ↔ a ≤ b

Tactic:
lt_castPred_iff,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
⊢ (a.pred ha).castSucc < b ↔ a ≤ b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
a : Fin (n + 1)
hb : a ≠ last n
h : a ≤ a
⊢ ↑(a.castPred ⋯ - a.castPred hb) = ↑(a - a) - 1

Tactic:
simp [val_sub, Nat.sub_add_cancel a.is_le]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ → #s = Fintype.card α

Tactic:
rintro rfl
    exact Finset.card_univ

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

Goal state before:
pp: α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
rw [sublist_iff_exists_orderEmbedding_getElem?_eq]

Goal state after:
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ Finite α

Tactic:
← finite_univ_iff,

Goal state after:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ univ.Finite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS : Insert.insert a s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯

Tactic:
rw [insert_subset_iff] at haS

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS✝ : Insert.insert a s ⊆ s✝
haS : a ∈ s✝ ∧ s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Infinite ↔ Infinite α

Tactic:
by
  simpa using (finite_range_iff hf).not

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ foldl (fun x y ↦ y * x) 1 s = foldl (fun x1 x2 ↦ x1 * x2) 1 s

Tactic:
by simp [mul_comm]

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

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
intro c

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c : α
⊢ ∀ {c_1 : α},
    r c c_1 →
      Relation.ReflTransGen r c_1 b →
        (∃ l, IsChain r (c_1 :: l) ∧ (c_1 :: l).getLast ⋯ = b) → ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ l.prod

Tactic:
by
  let ⟨s, t, h⟩ := append_of_mem ha
  rw [h, prod_append, prod_cons, mul_left_comm]
  exact dvd_mul_right _ _

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length

Tactic:
exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose k = n ! / (k ! * (n - k)!)

Tactic:
← choose_mul_factorial_mul_factorial hk,

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * k ! * (n - k)! / (k ! * (n - k)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !

Tactic:
← choose_mul_factorial_mul_factorial hk,

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * k ! * (n - k)!
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
subst eq; rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ piFinset s = ∅ ↔ ∃ i, s i = ∅

Tactic:
simp [piFinset]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ (piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty

Tactic:
simp [piFinset]

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

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S

Tactic:
rw [pow_zero]
    exact OneMemClass.one_mem S

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

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x

Tactic:
intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a⁻¹ * x) ((fun x ↦ a * x) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x

Tactic:
intro c

Goal state after:
case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a * x) ((fun x ↦ a⁻¹ * x) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b

Tactic:
intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b⁻¹) ((fun x ↦ x * b) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b

Tactic:
intro c

Goal state after:
case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x * b⁻¹) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x

Tactic:
intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ x⁻¹ * a) ((fun x ↦ a / x) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x

Tactic:
intro c

Goal state after:
case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a / x) ((fun x ↦ x⁻¹ * a) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b) fun x ↦ x / b

Tactic:
intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x / b) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b) fun x ↦ x / b

Tactic:
intro c

Goal state after:
case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x / b) ((fun x ↦ x * b) c) = c
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
· rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    exact ⟨n + m, zpow_add x n m⟩

Goal state after:
case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (insert 1 s) = closure s

Tactic:
by
  rw [insert_eq, closure_union]
  simp [one_mem]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y ↔ y⁻¹ * x ∈ f.ker

Tactic:
by
  constructor <;> intro h
  · rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y⁻¹ * x = 1
⊢ x = y

Tactic:
inv_mul_eq_one,

Goal state after:
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y = x
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Ker

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

Tactic:
le_bot_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ H = ⊥ ↔ 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 N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)

Tactic:
map_sup,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 = 1 ∧ ↑x.2 * (↑y.2)⁻¹ = 1
⊢ x = y

Tactic:
inv_mul_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑y.1 = ↑x.1 ∧ ↑x.2 * (↑y.2)⁻¹ = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f (a✝ * b✝) ∈ S

Tactic:
map_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f (x * y) = f x * f y

Tactic:
map_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f x * f y = f x * f y
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.boddDiv2 = (n.bodd, n.div2)

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [boddDiv2, ih]
    cases hn : n.bodd <;> simp [hn]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
| a ^ n.succ

Tactic:
← h.eq

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
| (a * a) ^ n.succ
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ map (↑(MulAut.conj 1)) H ≤ H

Tactic:
simp [MulAut.one_def]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
⊢ Monotone fun i ↦ (take i L).prod

Tactic:
refine monotone_nat_of_le_succ fun n => ?_
  rcases lt_or_ge n L.length with h | h
  · rw [prod_take_succ _ _ h]
    exact le_self_mul
  · simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

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

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨i✝, c⟩

Tactic:
· exact Lex.left _ _ hk

Goal state after:
case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨i✝, c⟩
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x y : α × β
⊢ toLex y < toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 < x.2

Tactic:
by
  rw [eq_comm, toLex_lt_toLex]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 = c.1 ∧ t.2 ≤ c.2
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
| inr h' =>

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

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = map (s.subtype.coprod t.subtype) (mrange (inl ↥s ↥t) ⊔ mrange (inr ↥s ↥t))

Tactic:
map_sup,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = map (s.subtype.coprod t.subtype) (mrange (inl ↥s ↥t)) ⊔ map (s.subtype.coprod t.subtype) (mrange (inr ↥s ↥t))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

Tactic:
induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g (a ⊔ b)) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
map_sup,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g a ⊔ g b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b