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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
g : M → N
f : ι → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : ι
⊢ (g ∘ f) x = 1 ↔ f x = 1

Tactic:
rw [Function.comp, hg (mem_range_self x)]

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

Goal state before:
pp: i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
cases (le_or_gt (2 : ℕ) i)

Goal state after:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

case inr
i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case refl
i : ℕ
⊢ i + 1! ≤ (i + 1)!

pp: case step
i h : ℕ
a✝ : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!

Tactic:
· exact self_le_factorial _

Goal state after:
case step
i h : ℕ
a✝ : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p.num ^ n) / ↑p.den ^ n = (↑p.num / ↑p.den) ^ n

Tactic:
Int.cast_pow,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑p.num ^ n / ↑p.den ^ n = (↑p.num / ↑p.den) ^ n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x < 1

Tactic:
refine lt_of_le_of_lt ?_ h

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ≤ 2 * fract x
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 ≤ ↑z - ↑⌊x⌋

Tactic:
le_sub_comm

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1
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
z a : ℤ
⊢ ↑a - ↑z ≤ a✝ ↔ ↑(a - z) ≤ a✝

Tactic:
Int.cast_sub

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a✝ : R
z a : ℤ
⊢ ↑a - ↑z ≤ a✝ ↔ ↑a - ↑z ≤ 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 b : R
⊢ ↑⌊a + b⌋ - 1 - a ≤ ↑⌊b⌋

Tactic:
refine le_trans ?_ (sub_one_lt_floor _).le

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 - a ≤ b - 1
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
⊢ ↑0 ≤ fract a ∧ fract a < ↑0 + 1

Tactic:
Int.cast_zero,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ 0 ≤ fract a ∧ fract a < 0 + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(c + 1) - fract (a * ↑(c + 1)) = ↑z

Tactic:
rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]

Goal state after:
case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
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:
Int.cast_zero,

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = - -(-↑n / ↑d)

Tactic:
neg_neg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = -↑n / ↑d
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 ≤ ↑⌈a + b⌉ + 1 - ↑⌈b⌉

Tactic:
le_sub_comm

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a
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 - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + (b - 1) * (b - 1)⁻¹

Tactic:
mul_inv_cancel₀

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 - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + 1

k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), count a ⟦_l₁⟧ = count a ⟦_l₂⟧

Tactic:
simp only [quot_mk_to_coe, coe_count]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
by
    convert! List.count_erase_self (a := a) (l := l) <;> rw [← coe_count] <;> simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ l₁.diff (a :: l₂) = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
by
    rw [diff_cons, (hl₁.erase _).sdiff_eq_filter, hl₁.erase_eq_filter, filter_filter]
    simp only [decide_not, bne, Bool.and_comm, decide_mem_cons, Bool.not_or]

Goal state after:
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:
by rw [singleton_disjoint]

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

Goal state before:
pp: α : Type u_1
s : List α
a : α
t : List α
⊢ s ∈ (a :: t).tails ↔ s <:+ a :: t

Tactic:
by
    simp only [tails, mem_cons, mem_tails s t]
    exact
      show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
        ⟨fun o =>
          match s, t, o with
          | _, t, Or.inl rfl => suffix_rfl
          | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
          fun e =>
          match s, t, e with
          | _, t, ⟨[], rfl⟩ => Or.inl rfl
          | s, t, ⟨b :: l, he⟩ =>
            List.noConfusion rfl (heq_of_eq he) fun _ lt => Or.inr ⟨l, eq_of_heq lt⟩⟩

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse l.tails).reverse

Tactic:
by
  rw [tails_eq_inits l]
  simp [← map_reverse]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.tails = l.reverse.inits.reverse

Tactic:
by
  rw [tails_eq_inits l]
  simp [← map_reverse]

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

Goal state before:
pp: α : Type u_5
s t : Finset α
h : Disjoint s t
a : α
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

Tactic:
rcases s with ⟨⟨s⟩⟩; rcases t with ⟨⟨t⟩⟩; apply List.mem_append

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = (a ::ₘ s.val).dedup

Tactic:
by
  rw [dedup_cons, dedup_eq_self]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), x ∉ {a} ∩ s

Tactic:
by
    simp only [mem_inter, mem_singleton]; rintro x ⟨rfl, h⟩; exact H h

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ sᶜ ↔ a ∉ s

Tactic:
mem_compl

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ s ↔ a ∉ s
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c

Tactic:
rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
    exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ Set.InjOn f ↑s

Tactic:
rw [Multiset.dedup_eq_self] at this

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).Nodup
⊢ Set.InjOn f ↑s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
f_inj : Set.InjOn f ↑s
⊢ #s ≤ #t

Tactic:
classical
  calc
    #s = #(s.image f) := (card_image_of_injOn f_inj).symm
    _ ≤ #t := card_le_card <| image_subset_iff.2 hf

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

Goal state before:
pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i < j.succ
⊢ r (f i) (f j.succ)

Tactic:
← le_castSucc_iff

Goal state after:
case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i ≤ j.castSucc
⊢ r (f i) (f j.succ)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #(t \ s ∪ s) - #s
⊢ #(t \ s) = #t - #s

Tactic:
by rwa [sdiff_union_of_subset h] at this

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

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

Tactic:
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.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
· rw [append_left, Function.comp_apply]
    refine congr_arg u (Fin.ext ?_)
    simp

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i < j.succ

Tactic:
← le_castSucc_iff

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i ≤ j.castSucc
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
constructor
  · intro H
    induction H with
    | slnil => simp
    | cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
      simpa using hf
    | cons_cons _ _ IH =>
      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 _
  · rintro ⟨f, hf⟩
    exact sublist_of_orderEmbedding_getElem?_eq f hf

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s

Tactic:
by
  rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]

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

Goal state before:
pp: case refine_2.cons
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂

Tactic:
· exact Or.inr ⟨rfl, h⟩

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

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ (map (fun x ↦ 1) m).prod = 1

Tactic:
rw [map_const', prod_replicate, one_pow]

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
rw [length_drop, length_drop, h]

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

Goal state before:
pp: case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]

Goal state after:
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
⊢ Disjoint (fun x ↦ p x.1 ∧ q x.2) fun x ↦ ¬p x.1 ∧ ¬q x.2

Tactic:
exact (disjoint_compl_right.inf_left _).inf_right _

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

Goal state before:
pp: case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose (n - r) ≤ n.choose (n / 2)

Tactic:
apply choose_le_middle_of_le_half_left

Goal state after:
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
by
  contrapose! +distrib
  rw [Set.infinite_image2 hfs hft]
  grind only [Set.Infinite.nonempty]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ 1 • b = b

Tactic:
by rw [← f.map_one, hsmul, one_smul]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_9
f : ι → α
a : α
⊢ a ∈ range f ↔ a ∈ ⋃ i, {f i}

Tactic:
by simp [@eq_comm α a]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
⊢ s ×ˢ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ×ˢ t i j

Tactic:
prod_iUnion

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun x ↦ f x b) '' s = image2 f s t

Tactic:
image2_swap,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun x ↦ f x b) '' s = image2 (fun a b ↦ f b a) t s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t

Tactic:
simp only [← image_prod, iUnion_prod_const, image_iUnion]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
by
    let ⟨x, hx⟩ := hsn
    simpa using hs x hx x hx

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ f.range = ⊥ ↔ f = 1

Tactic:
← le_bot_iff,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ f.range ≤ ⊥ ↔ f = 1
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) = map f (comap f (H ⊔ K))

Tactic:
by
      rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Tactic:
by
  rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self]
  exacts [le_sup_left, le_sup_right]

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

Goal state before:
pp: case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

Tactic:
exact lt_of_lt_of_le h (sqrt_le_self _)

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

Goal state before:
pp: motive : ℕ → Sort u
⊢ Function.Injective fun H n ↦ bitCasesOn n H

Tactic:
intro H₁ H₂ h

Goal state after:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂
⊢ H₁ = H₂
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑(map f (comap f H)) ≤ normalizer ↑H

Tactic:
map_comap_eq_self h

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑H ≤ normalizer ↑H
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) ^ 2 = (a ^ 2) ^ n.succ

Tactic:
← pow_mul,

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ map (↑(MulAut.conj g)) (⨅ g, map (↑(MulAut.conj g)) H) = ⨅ x, map (↑(MulAut.conj ((Equiv.mulLeft g) x))) H

Tactic:
map_iInf _ (MulAut.conj g).injective

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ⨅ i, map (↑(MulAut.conj g)) (map (↑(MulAut.conj i)) H) = ⨅ x, map (↑(MulAut.conj ((Equiv.mulLeft g) x))) H
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ∀ (x : Option α), ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) x = f x

Tactic:
by rintro (_ | _) <;> simp

Goal state after:
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → x = y

Tactic:
rw [Subtype.ext_iff]; exact @Std.Trichotomous.trichotomous α r _ x y

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

Goal state before:
pp: case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
⊢ (∃ (hm : x ∈ ⨆ i, S i), motive x hm) →
    (∃ (hm : y ∈ ⨆ i, S i), motive y hm) → ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm

Tactic:
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

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 ^ m.succ) ^ k = (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 ^ (m.succ * k) = (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
k : ℕ
⊢ (x ^ k) ^ n = 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
k : ℕ
⊢ x ^ (k * n) = 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ argAux r (foldl (argAux r) o tl) a
⊢ ¬r b m

Tactic:
argAux

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
⊢ ¬r b m
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type ?u.10
β : Type ?u.15
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
simp [decode_ofEquiv, encode_ofEquiv]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ maximum_of_length_pos h ∈ l

Tactic:
apply maximum_mem
  simp only [coe_maximum_of_length_pos]

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

Goal state before:
pp: α : Type u
a : α
⊢ ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
intro r₁

Goal state after:
α : Type u
a : α
r₁ : List (List α)
⊢ ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a ↑s) (max a (s.max' H))

Tactic:
exact (isGreatest_max' _ _).insert _

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists' = l.sublists' ++ map (cons a) l.sublists'

Tactic:
by
  simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]

Goal state after: