mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n

Tactic:
rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n - (↑i % n + 1) < n

Tactic:
exact i.modNat.rev.is_lt

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

Goal state before:
pp: n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
simpa [add_def] using Nat.mod_eq_of_lt (by lia)

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ (p.pred ⋯).predAbove i = i.castPred ⋯

Tactic:
by
  rw [predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + #sᶜ = Fintype.card α

Tactic:
card_add_card_compl

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ Fintype.card α = Fintype.card α
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l

Tactic:
rcases h with (⟨rfl | h⟩ | h)

Goal state after:
case refine_2.inl
α : Type u_1
l : List α
x : α
right✝ : x ∈ l
⊢ x ∈+ x :: l

case refine_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
⊢ hd :: tl <+ l'

Tactic:
have : ∀ ix, tl[ix]? = (l'.drop (f 0 + 1))[f' ix]? := by
    intro ix
    rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
    · simp only [getElem?_cons_succ]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact ix.succ_pos

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ hd :: tl <+ l'
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
⊢ ∃ f, map f univ = s

Tactic:
obtain ⟨f : α ↪ β, hf⟩ := exists_of_card_le_finset (Nat.le_of_eq hsn)
  use f
  apply Finset.eq_of_subset_of_card_le
  · simp [← coe_subset, hf]
  · simp [← hsn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x ↦ m (f x)) s = m (fold op b f s)

Tactic:
by
  rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
  simp only [Function.comp_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z

Tactic:
intro x y z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z

Tactic:
intro x y z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > min y z ↔ x > y ∨ x > z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z

Tactic:
intro x y z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ max y z ↔ x ≥ y ∧ x ≥ z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z

Tactic:
intro x y z

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > max y z ↔ x > y ∧ x > z
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
a b : M
h : Commute a b
z : M
⊢ b * (a * z) = a * (b * z)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
a b : M
h : Commute a b
z : M
⊢ b * a * z = a * (b * z)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
a b : M
h : Commute a b
z : M
⊢ b * a * z = a * (b * z)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
a b : M
h : Commute a b
z : M
⊢ b * a * z = a * b * z
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ ((a :: l).rotate n).prod = 1

Tactic:
have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
← rotate'_mod,

Goal state after:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' (n % l.length)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l

Tactic:
by
  rw [rotate_eq_rotate']
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

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

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
Nat.mod_eq_of_lt,

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

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
by
  classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _

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

Goal state before:
pp: k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
by simp [multichoose]

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

Goal state before:
pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S * (S ^ n * {a}), b * a⁻¹ ∈ S ^ n * {a}

Tactic:
← mul_assoc,

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S * S ^ n * {a}, b * a⁻¹ ∈ S ^ n * {a}
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ Subsingleton M

Tactic:
by
  constructor; intro x y
  have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
  exact absurd (this x) notMem_bot

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 β
f : α → β
⊢ MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)

Tactic:
by
  simp only [mapsTo_iInter]

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

Goal state before:
pp: case mem
M : Type u_1
inst✝ : Mul M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : y ∈ closure s
z : M
hz : z ∈ s
⊢ p z y ⋯ hy

Tactic:
induction hy using closure_induction with
    | mem _ h => exact mem _ _ hz h
    | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f✝ : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
η : Type v
R : Type w
s : ι → η
inst✝ : MulOneClass R
f g : ι → R
⊢ extend s (f * g) 1 = extend s f 1 * extend s g 1

Tactic:
by simpa using Function.extend_mul s f g 1 1

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
g : N →* G
hl : LeftInverse ⇑g ⇑f
hr : RightInverse ⇑g ⇑f
H : Subgroup G
⊢ ↑(map f H) = ↑(comap g H)

Tactic:
rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
P : Type u_8
inst✝ : MulOneClass P
g : N →* P
iso : G ≃* N
⊢ comap (↑iso) g.ker = map (↑iso.symm) g.ker

Tactic:
comap_equiv_eq_map_symm

Goal state after:
G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
P : Type u_8
inst✝ : MulOneClass P
g : N →* P
iso : G ≃* N
⊢ map (↑iso.symm) g.ker = map (↑iso.symm) g.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
exact h.trans
    ⟨fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨y * z * y⁻¹, hs.conj_mem z hz y, y, hy, by simp [hp]⟩,
    fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨z, hz, z⁻¹ * y * z, hs.conj_mem' y hy z, by simp [mul_assoc, hp]⟩⟩

Goal state after:
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)⁻¹ * (fun g ↦ ↑g.1 * ↑g.2) x = ↑y.2
⊢ x = y

Tactic:
← mul_assoc,

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
⊢ x = y
Module: Mathlib.Data.Countable.Defs

Goal state before:
pp: α : Sort u
inst✝ : Nonempty α
⊢ (¬∃ f, Surjective f) ↔ ∀ (f : ℕ → α), ¬Surjective f

Tactic:
not_exists

Goal state after:
α : Sort u
inst✝ : Nonempty α
⊢ (∀ (x : ℕ → α), ¬Surjective x) ↔ ∀ (f : ℕ → α), ¬Surjective f
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
⊢ map f (closure Set.univ) = mrange f

Tactic:
mrange_eq_map,

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
⊢ map f (closure Set.univ) = map f ⊤
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
x✝ : Subgroup G
⊢ zpowers g⁻¹ ≤ x✝ ↔ zpowers g ≤ x✝

Tactic:
simp only [zpowers_le, inv_mem_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * (h * g)) ↔ h ∈ s)

Tactic:
← mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * h * g) ↔ h ∈ s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ closure s ≤ closure (⇑↑(MulAut.conj h) '' s)

Tactic:
rw [closure_le, ← MonoidHom.map_closure]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(map (↑(MulAut.conj h)) (closure s))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * (c * b)⁻¹) ∈ H

Tactic:
← mul_assoc,

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a) * (c * b)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a * a = q * (a * a)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a * a = q * a * a
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, i ≠ j → (Disjoint on fun a ↦ a • s) i j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
disjoint_smul_set_right,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, i ≠ j → Disjoint (j⁻¹ • i • s) s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
φ : G₂ →* G₃
x : G₁
hx : x ∈ f.ker
⊢ (φ.comp f) x = 1

Tactic:
by simp [mem_ker.mp hx]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ mrange (FreeMonoid.lift f) = closure (Set.range f)

Tactic:
mrange_eq_map,

Goal state after:
M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ map (FreeMonoid.lift f) ⊤ = closure (Set.range f)
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
mrange_eq_map,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (map inl s + map inr t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t

Tactic:
map_add,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (map inl s) + map f (map inr t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : l.maximum = ↑y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Tactic:
| coe y =>

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
obtain hl | hl := hx
    · simp only [foldr]
      exact le_max_of_le_left h
    · exact le_max_of_le_right (IH (by assumption))

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← SupHom.comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f b = f a ⊔ f b

Tactic:
sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f b = f b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
⊢ s = ∅

Tactic:
obtain ⟨a, ha⟩ := max_of_nonempty H
      rw [h] at ha; cases ha;

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

Goal state before:
pp: case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ r.sup id ≤ z

Tactic:
exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

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

Goal state before:
pp: case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
simpa only [iSup_pos h] using by apply le_biSup _ h

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (i : β), ⨆ c, f (i, c) ≤ c

Tactic:
conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (b : β) (i : γ), f (b, i) ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
hf : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun i ↦ e (f i))

Tactic:
simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(s.preimage f hf) ⊆ ↑t

Tactic:
coe_preimage

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
⊢ ((t.preimage Subtype.val ⋯).sup fun x ↦ ↑x) = t.sup id

Tactic:
apply sup_preimage_self

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := ⋯
⊢ BijOn Subtype.val (Subtype.val ⁻¹' ↑t) ↑t
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
⊢ Set.range ⇑f = Set.range ⇑g ↔ f = g

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro rfl; rfl⟩
  let ef := (f.strictMono.strictMonoOn .univ).orderIso
  let eg := (g.strictMono.strictMonoOn .univ).orderIso
  let i : f '' .univ ≃o g '' .univ :=
    { __ := Equiv.setCongr (by simpa using! h)
      map_rel_iff' := by rfl }
  have : (ef.trans i).trans eg.symm = .refl _ := by
    exact Subsingleton.elim _ _
  ext x
  simpa only [OrderIso.trans_apply, OrderIso.apply_symm_apply, OrderIso.refl_apply, Subtype.ext_iff]
    using! congr(eg ($this ⟨x, Set.mem_univ x⟩))

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
⊢ a ≤ b ↔ b ∈ h₁_finset_Ici a

Tactic:
h₁_finset_mem_Ici

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
⊢ a ≤ b ↔ a ≤ b