mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : G
hx : x ∈ s
⊢ 1 ∈ s

Tactic:
simpa using hs x hx x hx

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

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

Tactic:
insert_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure ({1} ∪ s) = closure s
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K → map (↑e) K = H

Tactic:
rintro rfl

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) K = H → map (↑e.symm) H = K

Tactic:
rintro rfl

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K
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
⊢ ⇑f '' ↑H = ↑(comap g H)

Tactic:
coe_comap,

Goal state after:
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
⊢ ⇑f '' ↑H = ⇑g ⁻¹' ↑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 N
⊢ ⇑f '' ↑(comap f H) = ↑(f.range ⊓ H)

Tactic:
coe_comap,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ⇑f '' ⇑f ⁻¹' ↑H = ↑(f.range ⊓ H)
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 : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
⊢ ∃ a, (f.submonoidComap N') a = y

Tactic:
obtain ⟨x, hx⟩ := hf y
  use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩
  apply Subtype.val_injective
  simp [hx]

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

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp only [h₂, ↓reduceIte]

Goal state after:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h

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

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
simp only [h₂, ↓reduceIte]

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ {a, b} * s = a • s ∪ b • s

Tactic:
insert_eq,

Goal state after:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ ({a} ∪ {b}) * s = a • s ∪ b • s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ normalClosure ∅ = ⊥

Tactic:
by
  rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * {a, b} = s <• a ∪ s <• b

Tactic:
insert_eq,

Goal state after:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * ({a} ∪ {b}) = s <• a ∪ s <• b
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ (fun x ↦ a • x) ⁻¹' B = a⁻¹ • B

Tactic:
exact ((MulAction.toPerm _).image_symm_eq_preimage _).symm

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a = 1 → IsIdempotentElem a

Tactic:
rintro rfl

Goal state after:
M : Type u_1
inst✝ : Monoid M
h : IsUnit 1
⊢ IsIdempotentElem 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₃
⊢ (fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ) = φ

Tactic:
ext b
    simp [liftOfRightInverseAux, hf b]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ A ⊓ (B' ⊓ B))

Tactic:
inf_idem

Goal state after:
G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ (B' ⊓ B))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ A ⊓ (B ⊓ B))

Tactic:
inf_idem

Goal state after:
G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ A ⊓ B)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
· exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
⊢ S = ⊥ → card ↥S = 1

Tactic:
rintro rfl

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Fintype ↥⊥
⊢ card ↥⊥ = 1
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

pp: case inr.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩

Tactic:
· simpa using h.symm.ne_of_mem ha hb

Goal state after:
case inr.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: S : Set ℕ
⊢ S = Set.univ → 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S

Tactic:
rintro rfl

Goal state after:
⊢ 0 ∈ Set.univ ∧ ∀ (k : ℕ), k ∈ Set.univ → k + 1 ∈ Set.univ
Module: Mathlib.Order.Hom.BoundedLattice

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

Tactic:
comp_apply

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.swap.zero
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂
⊢ List.map (cons a) (powersetCardAux 0 l✝) ++ List.map (cons b) (powersetCardAux 0 (a :: l✝)) ~
    List.map (cons b) (powersetCardAux 0 l✝) ++ List.map (cons a) (powersetCardAux 0 (b :: l✝))

pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) (a :: l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) (b :: l✝))

Tactic:
· simp [Perm.swap]

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) (a :: l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) (b :: l✝))
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ (a :: l₁✝).sublists' <+ (a :: l₂✝).sublists'

Tactic:
sublists'_cons,

Goal state after:
case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' ++ map (List.cons a) l₁✝.sublists' <+ (a :: l₂✝).sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse
⊢ l₁ ++ l₂ ~ a :: l

Tactic:
sublists'_cons,

Goal state after:
case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip (l.sublists' ++ map (cons a) l.sublists').reverse
⊢ l₁ ++ l₂ ~ a :: l
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r

Tactic:
· intro H i hi j hj hij
    rcases mem_iUnion.1 hi with ⟨m, hm⟩
    rcases mem_iUnion.1 hj with ⟨n, hn⟩
    rcases hd m n with ⟨p, mp, np⟩
    exact H p (mp hm) (np hn) hij

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

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++
      flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    (h :: tl).sublists'

Tactic:
sublists'_cons,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++
      flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
rw [mem_prod] at hi hj

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ i = insert a j → i = j

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
j : Finset α
hj : j ⊆ s
hi : insert a j ⊆ s
⊢ insert a j = j
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ insert a i = j → i = j

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
hj : insert a i ⊆ s
⊢ i = insert a i
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))

Tactic:
intro i' hi' j' hj'

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))

Tactic:
intro i' hi' j' hj'

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ #a✝ = #a✝
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
⊢ P α

Tactic:
by
  cases nonempty_fintype α
  refine Fintype.induction_empty_option ?_ ?_ ?_ α
  exacts [fun α β _ => of_equiv, h_empty, @h_option]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : IsEmpty ι
inst✝ : InfSet α
f : ι → WithTop α
⊢ ⨅ i, f i = ⊤

Tactic:
rw [iInf, range_eq_empty, WithTop.sInf_empty]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ (⋃ j, I.pi fun i ↦ s i j) = I.pi fun i ↦ ⋃ j, s i j

Tactic:
by
  simp only [pi_def, biInter_eq_iInter, preimage_iUnion]
  have := hI.fintype.finite
  refine iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)
  exact preimage_mono <| hs i i.2 h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
z : β
hy : ⨆ c, f (z, c) ∈ range fun b ↦ ⨆ c, f (b, c)
⊢ ⨆ c, f (z, c) ≤ B

Tactic:
exact ciSup_le fun c ↦ by grind

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iio a = Iio ↑a

Tactic:
by
  rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]

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

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ i, f i = n → (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
rintro rfl

Goal state after:
case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
this : OrderBot α
⊢ (∃ i, f i = ⨅ i, f i) ∧ ∀ (i : ι), ⨅ i, f i ≤ f i
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
← mapsTo_univ_iff

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : MapsTo f univ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x y : α
inst✝ : PartialOrder α
hy : P y
hP : ∀ ⦃x : α⦄, P x → y ≤ x
⊢ x = y → Minimal P x

Tactic:
rintro rfl

Goal state after:
α : Type u_2
P : α → Prop
x : α
inst✝ : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x
Module: Mathlib.Order.Preorder.Finite

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

Tactic:
rintro rfl

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f : α ↪o β
⊢ Set.range ⇑f = Set.range ⇑f
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:
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.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
rintro rfl

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f : α →o β
hf hg : Function.Injective ⇑f
⊢ Set.range ⇑f = Set.range ⇑f
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc a b = 0 ↔ ¬a < b

Tactic:
by
  rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]

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

Goal state before:
pp: b : ℕ
⊢ #(Iic b) = b + 1

Tactic:
Iic_eq_Icc,

Goal state after:
b : ℕ
⊢ #(Icc ⊥ b) = b + 1
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
n k l : ℕ
ih : Set.InjOn (fun x ↦ x % 0) ↑(Ico n (n + 0))
hk : k ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hl : l ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hkl : k % 0 = l % 0
⊢ False
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h : P (x ^ n * x)
⊢ P (x ^ (n + 1))

Tactic:
by rwa [_root_.pow_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ b ∈ Ioc a ⟨y, ⋯⟩ ↔ a < b

Tactic:
by
    simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
    exact fun _ => b.property

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ ↑[[a, b]] = ↑(Icc a b ∪ Icc b a)

Tactic:
push_cast

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])

Tactic:
push_cast

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ center G = ⨅ g ∈ s, centralizer {g}

Tactic:
← centralizer_univ,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer Set.univ = ⨅ g ∈ s, centralizer {g}
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ g ∈ {g✝} → h * g * h⁻¹ ∈ {g✝}

Tactic:
rintro rfl

Goal state after:
case refine_2.refine_1
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {g}
⊢ h * g * h⁻¹ ∈ {g}
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ h * g * h⁻¹ ∈ {g✝} → g ∈ {g✝}

Tactic:
rintro rfl

Goal state after:
case refine_2.refine_2
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {h * g * h⁻¹}
⊢ g ∈ {h * g * h⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ g, g • H

Tactic:
ext g
  simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
  refine ⟨fun h x ↦ h x⁻¹, fun h x ↦ ?_⟩
  simpa only [ConjAct.toConjAct_inv, inv_inv] using! h x⁻¹

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ r x y

Tactic:
rw [← hr]; exact h c hS

Goal state after: