mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
rw [← NNRat.den_coe, ← Int.cast_natCast q.num, ← NNRat.num_coe]

Goal state after:
q : ℚ≥0
⊢ ↑q = ↑(↑q).num / ↑(↑q).den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ q.num ≠ 0 ↔ q ≠ 0

Tactic:
simp [num]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ = ↑(n₂ * ↑d₁)
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
← Int.cast_natCast d₂,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑↑d₂ = ↑(n₂ * ↑d₁)
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
q : ℚ
⊢ IsSquare q → IsSquare q.num ∧ IsSquare q.den

Tactic:
rintro ⟨qr, rfl⟩
    rw [Rat.mul_self_num, mul_self_den]
    simp only [IsSquare.mul_self, and_self]

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

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ (Int.ofNat a).pow b = Int.ofNat c

Tactic:
simp [← h1]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
s : Set α
l : α
⊢ l ≤ sSup s ↔ ∀ b < l, ∃ a ∈ s, b < a

Tactic:
by
  grind [sSup_lt_iff, mem_upperBounds, not_le]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
hκ : Nonempty κ
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i

Tactic:
rcases hκ with ⟨j⟩
  simp_rw [iInf_iSup_eq, mem_iInter]
  refine le_antisymm
    (iSup₂_le fun i hi ↦ le_iSup₂_of_le (fun _ ↦ i) hi (le_iInf fun _ ↦ le_rfl))
    (iSup₂_le fun I hI ↦ ?_)
  by_cases! H : ∀ k, I k = I j
  · exact le_iSup₂_of_le (I j) (fun k ↦ (H k) ▸ (hI k)) (iInf_le _ _)
  · rcases H with ⟨k, hk⟩
    calc ⨅ l, f (I l)
    _ ≤ f (I k) ⊓ f (I j) := le_inf (iInf_le _ _) (iInf_le _ _)
    _ = ⊥ := (h hk).eq_bot
    _ ≤ _ := bot_le

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
⊢ lhs ≤ rhs

Tactic:
suffices rhs ≥ x from nomatch not_lt.2 this hr

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
⊢ rhs ≥ x
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ (∀ a_1 ∈ Iic a, ∃ a_2 ∈ Iic a, a_1 ⊓ a_2 = ⊥ ∧ a_1 ⊔ a_2 = a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
Set.mem_Iic

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

Goal state before:
pp: case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i ↦ f i, x ≤ y

Tactic:
rintro x ⟨-, ⟨i, rfl⟩, hi⟩

Goal state after:
case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
x : α
i : ι
hi : x ∈ (fun i ↦ Iic (f i)) i
⊢ ∃ y ∈ range fun i ↦ f i, x ≤ y
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ (∀ (x : ι), ¬x ∈ ∅ → f x = 1) ↔ f = 1

Tactic:
funext_iff

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ (∀ (x : ι), ¬x ∈ ∅ → f x = 1) ↔ ∀ (x : ι), f x = 1 x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
h : ↑m = ↑k * 0
⊢ False

Tactic:
simp only [mul_zero, ne_zero] at h

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
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ |a - b| < 1

Tactic:
calc |a - b|
    _ = a - b := abs_of_nonneg (sub_nonneg_of_le h0)
    _ < ⌊a⌋ + 1 - b := sub_lt_sub_right (lt_floor_add_one a) _
    _ ≤ ⌊a⌋ + 1 - ⌊b⌋ := sub_le_sub_left (floor_le b) _
    _ = 1 := by rw [h, add_sub_cancel_left]

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⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋

Tactic:
exact mod_cast le_floor_add_floor a b

Goal state after:
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✝
⊢ ∃ n, x ≤ x✝ ^ n

Tactic:
by
    refine (MulArchimedean.arch (f x) (by simpa using hf h)).imp ?_
    simp [← map_pow, hf.le_iff_le]

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
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - fract a

Tactic:
by
  rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
  abel

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
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - fract a

Tactic:
by
  rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
  abel

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

Goal state before:
pp: case below
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
⊢ ∃ n, ↑n ≤ x

Tactic:
obtain ⟨n, hn⟩ := exists_int_lt x

Goal state after:
case below
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
hn : ↑n < x
⊢ ∃ n, ↑n ≤ x
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inl
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < c ^ 0 ∧ c ^ 0 < b

Tactic:
rw [zpow_zero]

Goal state after:
case inr.inr.inl
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < 1 ∧ 1 < b
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Torsor G P
inst✝ : Torsor G' P'
s₁ s₂ : Set P
t₁ t₂ : Set P'
⊢ s₁ ×ˢ t₁ /ₛ s₂ ×ˢ t₂ = (s₁ /ₛ s₂) ×ˢ (t₁ /ₛ t₂)

Tactic:
aesop (add norm simp [mem_sdiv, mem_prod])

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

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ≤ t
⊢ s ∪ t = t

Tactic:
rw [union_comm, eq_union_left h]

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

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

Tactic:
rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
  · simp only [Multiset.add_zero]
  · simp [-Bool.not_eq_true, -not_and]
  · simp only [implies_true, Decidable.em]

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

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

Tactic:
by
  rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
  · simp only [Multiset.add_zero]
  · simp [-Bool.not_eq_true, -not_and]
  · simp only [implies_true, Decidable.em]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) =
    countP p (filter q (Quot.mk (⇑(isSetoid α)) l)) + countP p (filter (fun a ↦ ¬q a) (Quot.mk (⇑(isSetoid α)) l))

Tactic:
convert! l.countP_eq_countP_filter_add (p ·) (q ·)

Goal state after:
case e'_3.e'_6
α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countP p (filter (fun a ↦ ¬q a) (Quot.mk (⇑(isSetoid α)) l)) =
    List.countP (fun x ↦ decide (p x)) (List.filter (fun a ↦ !decide (q a)) l)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint (ndinsert a s) t ↔ _root_.Disjoint (a ::ₘ s) t

Tactic:
by simp [disjoint_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
⊢ (replicate n a).toFinset = {a}

Tactic:
ext x
  simp [hn, List.mem_replicate]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ image f s = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Data.Finset.Card

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

Tactic:
rw [← (card_filter_le s p).ge_iff_eq, eq_iff_card_le_of_subset (filter_subset p s),
    filter_eq_self]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < ↑a ↔ a ≠ 0

Tactic:
Nat.pos_iff_ne_zero,

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ ↑a ≠ 0 ↔ a ≠ 0
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: m n : ℕ
h : n = m
⊢ (castOrderIso h).symm = castOrderIso ⋯

Tactic:
by subst h; rfl

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

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = (↑↑u - ↑↑v) % ↑n

pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n

Tactic:
· rw [Int.emod_eq_of_lt] <;> omega

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
obtain ⟨a, ha, rfl⟩ := i_surj b h

Goal state after:
case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ i a ha ∈ image (fun a ↦ i ↑a ⋯) s.attach
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ #s ≤ #t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
have hmapsto' : Set.MapsTo f' s.attach t := fun x hx ↦ hf _ _

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = [].concat (f (Fin.last 0))

Tactic:
concat_nil,

Goal state after:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = [f (Fin.last 0)]
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑(a - b)

Tactic:
have : b.castLT (lt_of_le_of_lt h ha) ≤ a.castLT ha := by simpa [← val_fin_le] using h

Goal state after:
n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
this : b.castLT ⋯ ≤ a.castLT ha
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑(a - b)
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
le_castSucc_iff

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < i.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p ≤ i.castSucc ↔ p < i.succ

Tactic:
le_castSucc_iff

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < i.succ ↔ p < i.succ
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: a b : Fin 2
⊢ a = b → (a = 0 ↔ b = 0)

Tactic:
by rintro rfl; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ (fun i ↦ #(g i) - 1) j ≤ (fun i ↦ #(g i) - 1) i

Tactic:
dsimp; gcongr #?_ - 1; exact hg h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ (fun i ↦ #(g i) - 1) j ≤ (fun i ↦ #(g i) - 1) i

Tactic:
by dsimp; gcongr #?_ - 1; exact hg h

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth x (p.removeNth f) = update f p x

Tactic:
simp [Fin.insertNth_eq_iff]

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

Goal state before:
pp: n : ℕ
α : Type u_3
p : Fin (n + 1)
x : α
f : Fin n → α
⊢ range (p.insertNth x f) = Set.insert x (range f)

Tactic:
ext y
  simp [Fin.exists_iff_succAbove p, Set.insert, eq_comm]

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Finite α

Tactic:
nontriviality α

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
⊢ Finite α
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ (a :: l).rotate n = a :: l

Tactic:
hb,

Goal state after:
α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ (replicate (a :: l).length b).rotate n = replicate (a :: l).length b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
rcases hk' : k with - | k'

Goal state after:
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
hk' : k = 0
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Tactic:
refine ext_get this fun n hn hn' => ?_

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.get ⟨n, hn⟩ = (l.cyclicPermutations.rotate k).get ⟨n, hn'⟩
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case mp
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) → (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y

Tactic:
rintro ⟨i, hi, j, hj, hne, rfl, rfl⟩

Goal state after:
case mp
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne : ¬i = j
⊢ (∃ i_1 h, l[i_1] = l[i]) ∧ (∃ i h, l[i] = l[j]) ∧ ¬l[i] = l[j]
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Disjoint s.diag s.offDiag

Tactic:
by simp [disjoint_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ (f '' ∅ᶜ)ᶜ = (range f)ᶜ

Tactic:
compl_empty,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ (f '' univ)ᶜ = (range f)ᶜ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = t ∪ kernImage f s

Tactic:
kernImage_union_preimage,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f s ∪ t = t ∪ kernImage f s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ x = y

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
      (show f x ∈ Set.iUnion U by rw [hU]; trivial)

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y
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
⊢ 1 ∈ S

Tactic:
exact OneMemClass.one_mem S

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
hb : b✝ = 1
ha : a✝ = 1
⊢ 1 * b✝ = 1

Tactic:
hb,

Goal state after:
M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
hb : b✝ = 1
ha : a✝ = 1
⊢ 1 * 1 = 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Tactic:
by
  simp_rw [iUnion_inter, inter_iUnion]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ (fun x ↦ x⁻¹) '' s = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s = ∅ ↔ 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 s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Tactic:
by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i => mem_image2_of_mem hx (hy _)

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x ↦ x * a) ⁻¹' {b} = {b * a⁻¹}

Tactic:
by
  rw [← image_mul_right', image_singleton]

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.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f a * f (b * y) = f a * f b * f y

Tactic:
hb,

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.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f a * (f b * f y) = f a * f b * f y
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 : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
hb,

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ b * n * b⁻¹ ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

Tactic:
← Set.singleton_union,

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