mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ Iio a = range a

Tactic:
Iio_eq_range

Goal state after:
a : ℕ
⊢ range a = range a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (↑(Ico a b)).Nonempty ↔ a < b

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Set.Ico a b).Nonempty ↔ a < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ico a b) = ∅ ↔ ¬a < b

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b = ∅ ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ ↑(Ico a₂ b) ⊆ ↑(Ioo a₁ b)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ ↑(Ioo a₁ b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ico a b) ⊆ ↑(Icc a b)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b ↑(Ico a b) = Set.Icc a b

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Set.Ico a b) = Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Set.Ioo a b) = ↑(Ico a b)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Set.Ioo a b) = Set.Ico a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ ↑(Ico a₁ b₁) ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Set.Ico a₁ b₁ ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Set.Ico a₁ b₁ ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ ↑(Ico a b) ∪ ↑(Ico b c) = ↑(Ico a c)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Set.Ico a b ∪ ↑(Ico b c) = ↑(Ico a c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Set.Ico a b ∪ ↑(Ico b c) = ↑(Ico a c)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Set.Ico a b ∪ Set.Ico b c = ↑(Ico a c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Set.Ico a b ∪ Set.Ico b c = ↑(Ico a c)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Set.Ico a b ∪ Set.Ico b c = Set.Ico a c
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ ↑(Ico a b) ∪ ↑(Ico b c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ ↑(Ico a b) ∪ ↑(Ico b c)

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ ↑(Ico b c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ ↑(Ico a b) ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico a b ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico a b ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico a b ∪ Set.Ico c d = ↑(Ico (min a c) (max b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico a b ∪ Set.Ico c d = ↑(Ico (min a c) (max b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ ↑(Ico a b) ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Set.Ico a b ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Set.Ico a b ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Set.Ico a b ∪ Set.Ico c d = ↑(Ico (min a c) (max b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Set.Ico a b ∪ Set.Ico c d = ↑(Ico (min a c) (max b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ico a b) ∩ ↑(Ico c d) = ↑(Ico (max a c) (min b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico a b ∩ ↑(Ico c d) = ↑(Ico (max a c) (min b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico a b ∩ ↑(Ico c d) = ↑(Ico (max a c) (min b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico a b ∩ Set.Ico c d = ↑(Ico (max a c) (min b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico a b ∩ Set.Ico c d = ↑(Ico (max a c) (min b d))

Tactic:
coe_Ico,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico a b ∩ Set.Ico c d = Set.Ico (max a c) (min b d)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ z * (a * c) = a * c * z

Tactic:
h.comm

Goal state after:
M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * c * z = a * c * z
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : h ∈ s
⊢ g * h * g⁻¹ ∈ s

pp: case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s

Tactic:
· simpa [← hg h hh]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x

Tactic:
convert! (prod_map s σ.toEmbedding f).symm
  exact (map_perm hs).symm

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y ↦ h • y) '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ g * x) ⁻¹' (fun y ↦ h • y) '' s

Tactic:
by
  simp [preimage_preimage, mul_assoc]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)

Tactic:
rw [← h₂ _ hx, ← h₂ _ hy]

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
by
  rw [← Finset.prod_filter]; congr; grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
⊢ ∏ x, f x = f a

Tactic:
have : Unique ι := uniqueOfSubsingleton a
  rw [prod_unique f, Subsingleton.elim default a]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
⊢ (lift ⇑f) (x * 0) = (lift ⇑f) x * (lift ⇑f) 0

Tactic:
simp only [mul_zero, map_zero]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : M
⊢ mk (x * y) 1 = mk x 1 * mk y 1

Tactic:
by rw [mk_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : a * ↑x < ⊥ * ↑x
⊢ a < ⊥

Tactic:
rw [bot_mul x0'] at h

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : a * ↑x < ⊥
⊢ a < ⊥
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j.pred.succ] ⊥)

Tactic:
simp only [Function.iterate_succ', Function.comp_apply]

Goal state after:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ (Order.succ^[j.pred] ⊥))
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ Ioo a b = ∅ ↔ b ≤ succ a

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩
  · ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ x < 2 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2

Tactic:
lt_two_iff,

Goal state after:
α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ x ≤ 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
a : ℕ∞
a✝ : ℕ
h : a < ↑a✝
⊢ a ≤ ↑a✝ - 1

Tactic:
· exact ENat.le_sub_of_add_le_right one_ne_top <| lt_natCast_add_one_iff.mp <|
      lt_tsub_iff_right.mp h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.fst, x.snd)

Tactic:
apply prod_equiv (Equiv.sigmaEquivProd _ _).symm

Goal state after:
case hst
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ (i : γ × α), i ∈ r ↔ (Equiv.sigmaEquivProd γ α).symm i ∈ s.sigma t

case hfg
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ i ∈ r, f i = f (((Equiv.sigmaEquivProd γ α).symm i).fst, ((Equiv.sigmaEquivProd γ α).symm i).snd)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, f ↑i ⋯

Tactic:
by
  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)

Tactic:
simp_rw [apply_ite k]

Goal state after:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (g x)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)

Tactic:
simp_rw [apply_ite k]

Goal state after:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (f x)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨hba⟩ | ⟨hba⟩ | ⟨b, a⟩)

Goal state after:
case refine_1.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁✝ a₂✝ : α
hba : a₁✝ ≤ a₂✝
hab : inl a₂✝ < inl a₁✝
⊢ False

case refine_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hba : b₁✝ ≤ b₂✝
hab : inr b₂✝ < inr b₁✝
⊢ False

case refine_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case h.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
gt : s (↑(collapseF f m)) b
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

Tactic:
· exact (hm gt).elim

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ {y | IsExtremePt x f y}

pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}

Tactic:
· refine ⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩
      intro y hy hyx
      exfalso
      exact lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)

Goal state after:
case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ g '' (f '' s)ᶜ

Tactic:
by rwa [hns]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
by rwa [hns]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
by rwa [hns]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ CharZero Cardinal.{u_1}

Tactic:
refine ⟨fun a b h ↦ ?_⟩

Goal state after:
α β : Type u
a b : ℕ
h : ↑a = ↑b
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ 1 < #α ↔ Nontrivial α

Tactic:
by
  rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∃ n, c = ↑n

Tactic:
rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩
    rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩
    suffices S.Finite by
      lift S to Finset ℕ using this
      simp
    contrapose! h'
    have := Infinite.to_subtype h'
    exact ⟨Infinite.natEmbedding S⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

pp: case refine_2
a b : Cardinal.{u_1}
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀

Tactic:
· by_cases ha : a = 0
    · exact Or.inl ha
    right
    by_cases hb : b = 0
    · exact Or.inl hb
    right
    rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb
    constructor
    · rw [← mul_one a]
      exact (mul_le_mul' le_rfl hb).trans_lt h
    · rw [← one_mul b]
      exact (mul_le_mul' ha le_rfl).trans_lt h

Goal state after:
case refine_2
a b : Cardinal.{u_1}
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ ↑n < ℵ₀

Tactic:
rw [power_natCast, ← Nat.cast_pow]; apply natCast_lt_aleph0

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable ↑s)

Tactic:
rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ #↑s

Tactic:
← lift_id #(↑s)

Goal state after:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ lift.{u, u} #↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)

Tactic:
← lift_id #(↑s)

Goal state after:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x y : R) (b : A), (x * y) • b = x • y • b

Tactic:
simp [smul_def', mul_assoc]

Goal state after: