mathlib-initiative/mathlib-tactics huggingface dataset:
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).castLT ⋯)

Tactic:
exact val_sub_castLT_of_le ha h

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f

Tactic:
by
  intro x
  have := Classical.propDecidable
  cases nonempty_fintype α
  have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _)
      ((card_image_of_injective univ hinj).symm ▸ le_rfl)
  have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
  obtain ⟨y, h⟩ := mem_image.1 h₂
  exact ⟨y, h.2⟩

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

Goal state before:
pp: case cast
n : ℕ
P : Fin (n + 1) → Prop
i✝ : Fin n
hi : P i✝.castSucc
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
| cast _ =>

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).Finite

Tactic:
by
  rw [Set.Finite] at hs ht
  apply toFinite

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
classical
    rw [duplicate_iff_two_le_count, ← replicate_sublist_iff,
      sublist_iff_exists_fin_orderEmbedding_get_eq]
    constructor
    · rintro ⟨f, hf⟩
      refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
      rw [← hf, ← hf]; simp
    · rintro ⟨n, m, hnm, h, h'⟩
      refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
      · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]
      · rintro ⟨⟨_ | i⟩, hi⟩
        · simpa using h
        · simpa using h'

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

Goal state before:
pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)

Tactic:
← cons_erase h,

Goal state after:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s.erase a) = op a (fold op b (a ::ₘ s.erase a))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
set u : ℕ → γ := fun n ↦ Nat.strongRecOn n f

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
⊢ ∃ a ∈ s, a ∉ t

Tactic:
by_contra! h; exact hs <| ht.subset h

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton (insert a s) = insert a s

Tactic:
| insert a s has ih =>

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
⊢ Pairwise R l

Tactic:
by
  rw [pairwise_iff_forall_sublist]
  intro a b hab
  if heq : a = b then
    cases heq; apply refl
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
⊢ R (l.get a) (l.get b)

Tactic:
obtain rfl | hlt := Fin.eq_or_lt_of_le hab

Goal state after:
case inl
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a : Fin l.length
hab : a ≤ a
⊢ R (l.get a) (l.get a)

case inr
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ R (l.get a) (l.get b)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = map f 0

Tactic:
map_zero

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = 0
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset ι
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
g : ι → M
⊢ map (fun i ↦ f (g i)) s = map (⇑f) (map g s)

Tactic:
exact (map_map _ _ _).symm

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

Goal state before:
pp: α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
cons_product,

Goal state after:
α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + s ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
simp [add_left_comm, add_assoc]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1) * n.choose (k + 1)

Tactic:
mul_add_one,

Goal state after:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) =
    (n + 1).choose (k + 1) * (k + 1) + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ ↑(s ∩ t).offDiag = ↑(s.offDiag ∩ t.offDiag)

Tactic:
by
    push_cast
    exact Set.offDiag_inter _ _

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

Goal state before:
pp: case neg.hf.hf
α : 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'
b : β a
a✝ : b ∈ t a
⊢ ∀ (a_1 : β a'),
    a_1 ∈ t a' →
      map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n ≍
        map (fun x ↦ Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n

Tactic:
intro b' _

Goal state after:
case neg.hf.hf
α : 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'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' x)) n ≍ map (fun x ↦ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b x)) n
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
⊢ IsPretransitive G X

Tactic:
constructor
  intro x y
  rcases ha x with ⟨g, rfl⟩
  rcases ha y with ⟨h, rfl⟩
  exact ⟨h * g⁻¹, by simp [mul_smul]⟩

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

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)

pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
· infer_instance

Goal state after:
case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)
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)
x : G
⊢ x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)

Tactic:
hx

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)
x : G
hx : x ∈ S ^ (n + 1)
⊢ x * a * a⁻¹ ∈ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : SemiconjBy (↑c) 1 a
⊢ a = 1

Tactic:
rw [SemiconjBy, mul_one] at h

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : ↑c = a * ↑c
⊢ a = 1
Module: Mathlib.Data.Set.Lattice.Image

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

Tactic:
by
  rw [kernImage_eq_compl, compl_compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default = x i

Tactic:
replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ j, s j
⊢ x default = x i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
⊢ x ∈ ⋃ i, s i → ∀ ⦃x₂ : α⦄, x₂ ∈ ⋃ i, s i → f x = f x₂ → x = x₂

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ i, s i
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ ⋃ i, s i → f x = f x₂ → x = x₂
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
intro x hz x' hw
    exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ x ∈ ↑(closure s) → x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
hx

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)

Tactic:
exact Subsemigroup.closure_le.mpr subset_closure hx

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

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

Tactic:
inf_subgroupOf_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = H.subgroupOf K
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) K
x : G
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

Tactic:
have : Nonempty K := Kne.to_subtype

Goal state after:
G : Type u_1
inst✝ : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : Nonempty ↑K
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
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
⊢ map f H = ⊥ ↔ H = ⊥

Tactic:
map_eq_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 ≤ f.ker ↔ 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 : Subgroup G
x : G
⊢ x ∈ comap f (map f H) → x ∈ H ⊔ f.ker

Tactic:
hx

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ⊓ H₂ ≤ ⊥ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1

Tactic:
simp only [SetLike.le_def, mem_inf, mem_bot, and_imp]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inr M N) = ⊥.prod ⊤

Tactic:
simpa only [mrange_eq_map] using map_inr ⊤

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

Tactic:
by
  simp_rw [SetLike.ext'_iff]
  exact Set.univ_pi_eq_singleton_iff

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
rw [← shiftRight_add, Nat.add_comm] at this

Goal state after:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ encode ((decode₂ α x).get h) = x

Tactic:
by rw [← decode₂_isPartialInv (Option.get _ h), Option.some_get]

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

Tactic:
by
  simp_rw [SetLike.ext'_iff]
  exact Set.univ_pi_eq_singleton_iff

Goal state after:
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 : G →* N
x : N
⊢ x ∈ map f (normalizer ↑H) → x ∈ normalizer ↑(map f H)

Tactic:
hx

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : N
hx : x ∈ map f (normalizer ↑H)
⊢ x ∈ normalizer ↑(map f H)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ S ≤ powers a

Tactic:
rintro _ (rfl | rfl); exacts [one_mem _, Submonoid.mem_powers _]

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ x ∈ s →
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z

Tactic:
hx

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
⊢ ∀ (y : M),
    (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a

Tactic:
hx

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
⊢ ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ y ∈ closure {x} ↔ ∃ n, n • x = y

Tactic:
rw [closure_singleton_eq, AddMonoidHom.mem_mrange]

Goal state after:
A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : β
⊢ x✝ ∈ u.toRight → x✝ ∈ v.toRight

Tactic:
simpa only [mem_toRight] using @h _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
⊢ x ∈ s → ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
hx

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
⊢ ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
⊢ x ∈ ↑s → ∀ ⦃b : α⦄, b ∈ ↑s → x < b → f x < f b

Tactic:
hx

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
⊢ ∀ ⦃b : α⦄, b ∈ ↑s → x < b → f x < f b
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ l'.revzip = List.map (fun x ↦ (x, ↑l - x)) l'

Tactic:
rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun a c ↦ a = (c, ↑l - c)) l'.revzip l'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) l).length + (map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)

Tactic:
length_sublistsLen (n + 1) l,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose (n + 1) + (map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ (map l.get (finRange l.length)).sublists'

Tactic:
sublists'_map

Goal state after:
α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
⊢ x ∈ S → ∀ ⦃y : α⦄, ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y

Tactic:
hx

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
⊢ ∀ ⦃y : α⦄, ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
⊢ x ∈ u → x ∈ (powersetCard n.succ u).biUnion id

Tactic:
hx

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ x ∈ (powersetCard n.succ u).biUnion id
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]

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

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
⊢ x ∈ s → f x < a

Tactic:
hx

Goal state after:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
⊢ x ∈ s → a < f x

Tactic:
hx

Goal state after:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ a < f x
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
⊢ f a ⩿ f b

Tactic:
refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
  obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
  rw [f.lt_iff_lt] at ha hb
  exact hab.2 ha hb

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (fun x1 x2 ↦ x1 ⩿ x2) = ReflGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
ext x y

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x ⩿ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y