mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
s : Finset α✝
t : Finset β✝
s₁ s₂ : Finset α✝
t₁ t₂ : Finset β✝
a✝ : α✝
b✝ : β✝
x : α✝ ⊕ β✝
u v : Finset (α✝ ⊕ β✝)
a : α✝
b : β✝
α : Type u_4
β : Type u_5
⊢ ∀ {a b : Finset (α ⊕ β)},
    { toFun := fun s ↦ (s.toLeft, s.toRight), invFun := fun s ↦ s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun s ↦ (s.toLeft, s.toRight), invFun := fun s ↦ s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ⊆ b

Tactic:
by simp [← Finset.coe_subset, Set.subset_def]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ f ⊥ = ⊥

Tactic:
map_bot

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ ⊥ = ⊥
Module: Mathlib.Data.List.Sublists

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

Tactic:
length_map,

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)

Tactic:
refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
← hs.coe_toFinset,

Goal state after:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : ↑hs.toFinset ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Ico a b = {c}
⊢ a = c ∧ a ⋖ b

Tactic:
simp_rw [Set.ext_iff, mem_Ico, mem_singleton_iff] at h

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x = c
⊢ a = c ∧ a ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Ico a b = {c}
⊢ a = c ∧ a ⋖ b

Tactic:
by
    simp_rw [Set.ext_iff, mem_Ico, mem_singleton_iff] at h
    have ⟨hac, hcb⟩ := (h c).mpr rfl
    obtain rfl := (h a).mp ⟨le_refl a, hac.trans_lt hcb⟩
    exact ⟨rfl, ⟨hcb, fun d hcd hdb ↦ hcd.ne ((h d).mp ⟨hcd.le, hdb⟩).symm⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)

Tactic:
by rw [gc.l_csSup hne hbdd, sSup_image']

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
refine Or.inl (subset_antisymm ?_ hst)

Goal state after:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t ⊆ s
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case h
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
b c : α
hc : c ∈ s
hbc : b ≤ c
⊢ b ≤ a

Tactic:
exact hbc.trans (ha.le hc)

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ {a}.val = {a}

Tactic:
Finset.singleton_val

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ {a} = {a}
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩

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

Goal state before:
pp: a x : ℕ
⊢ x < a ↔ x ∈ Finset.range a

Tactic:
Finset.mem_range

Goal state after:
a x : ℕ
⊢ x < a ↔ x < a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Ico (n✝ - n✝) (n✝ + 1) = Ico 0 (n✝ + 1)

Tactic:
Nat.sub_self

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
exact Set.Icc_ssubset_Icc_left hI ha hb

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ ∀ (f_1 : ℕ → β), (∀ (n : ℕ), f_1 n ∈ f '' s) → ∃ m n, m < n ∧ r' (f_1 m) (f_1 n)

Tactic:
intro g' hg'

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
· rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ WellQuasiOrderedLE { x // x ∈ s } ↔ IsWellFounded { x // x ∈ s } fun x1 x2 ↦ x1 < x2

Tactic:
wellQuasiOrderedLE_iff_wellFoundedLT

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ WellFoundedLT { x // x ∈ s } ↔ IsWellFounded { x // x ∈ s } fun x1 x2 ↦ x1 < x2
Module: Mathlib.Algebra.Group.Center

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

Tactic:
h.comm,

Goal state after:
M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * (c * z)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ x✝ ∈ center Mˣ

Tactic:
rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
m : Gᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
rwa [← op_closure] at hm

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

Goal state before:
pp: case e'_3
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ s = map (Equiv.toEmbedding σ) s

Tactic:
exact (map_perm hs).symm

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:
by rw [← hr]; exact h c hS

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

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
H3 : tl ++ x✝⁵ = tl2 ++ x✝⁴
⊢ (x3, b3) :: tl ++ x✝⁵ = (x4, b4) :: tl2 ++ x✝⁴

Tactic:
simp [H1, H3]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι × ι → M
⊢ ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)

Tactic:
simp [diag]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

Tactic:
rw [union_comm, prod_union_eq_left hs]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)

Tactic:
rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f✝ g✝ : F
x✝ : α
f g : F
x : α
hfg : f x⁻¹ ≤ g x⁻¹
⊢ g x = f x * (f x⁻¹ * g x)

Tactic:
by simp [← mul_assoc, ← map_mul]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
⊢ ↑s₃' * (↑s₂' * (r₂ * r₁)) = r₃' * r₁' * ↑s₂

Tactic:
← mul_assoc _ r₂,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
⊢ ↑s₃' * (↑s₂' * r₂ * r₁) = r₃' * r₁' * ↑s₂
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
s s' : ↥S
⊢ ↑s /ₒ s' * (↑s' /ₒ s) = 1

Tactic:
simp [oreDiv_mul_char (s : R) s' s' s 1 1 (by simp)]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (f ms₂.1 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = f ms₂.1 * f ↑ms₁.2

Tactic:
simp_rw [← map_mul, eq_iff_exists] at eq ⊢

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : ∃ c, ↑c * (m * (ms₁.1 * ↑ms₂.2)) = ↑c * (m * (ms₂.1 * ↑ms₁.2))
⊢ ∃ c, ↑c * (ms₁.1 * ↑ms₂.2) = ↑c * (ms₂.1 * ↑ms₁.2)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]

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

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b

Tactic:
succ_eq_succ,

Goal state after:
m n a b : ℕ
h : a ≤ b
⊢ succ^[b - a] a = b
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.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.snd, x.fst)

Tactic:
apply prod_equiv ((Equiv.prodComm _ _).trans (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.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ (i : α × γ), i ∈ r ↔ ((Equiv.prodComm α γ).trans (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.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ i ∈ r,
    f i =
      f
        ((((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i).snd,
          (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i).fst)
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p2, seq := s2, seqLeft := sl2, seqRight := sr2 }

Tactic:
obtain rfl : @p1 = @p2 := by
      funext α x
      apply H1

Goal state after:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p1, seq := s2, seqLeft := sl2, seqRight := sr2 }
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ s1 = s2

Tactic:
by
      funext α β f x
      exact H2 f (x Unit.unit)

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ l.length - 1 = n - 1

Tactic:
rw [p]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < l.length

Tactic:
rw [p]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < n
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : AddConst α (α✝ → β✝)
x✝ : α✝
⊢ x✝¹ <*> pure x✝ = (fun h ↦ h x✝) <$> x✝¹

Tactic:
by simp [Const.map, map, Seq.seq, pure, add_zero]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ↑s = Multiset.replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
Multiset.eq_replicate

Goal state after:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ((↑s).card = n ∧ ∀ b ∈ ↑s, b = a) ↔ ∀ b ∈ s, b = a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
v : Vector α 1
⊢ v.toList = [v.head]

Tactic:
rw [← v.cons_head_tail]

Goal state after:
α : Type u_1
v : Vector α 1
⊢ (v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
⊢ (a ::ᵥ v).get i.succ = v.get i

Tactic:
rw [← get_tail_succ, tail_cons]

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t', ht'⟩) ∈ f t'

Tactic:
exact hF ⟨t', _⟩

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ inr ⊤

Tactic:
· exact Lex.inr le_top

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

Goal state before:
pp: ι : Type u
c : ι → Cardinal.{v}
⊢ lift.{w, max v u} (prod c) = prod fun i ↦ lift.{w, v} (c i)

Tactic:
lift c to ι → Type v using fun _ => trivial

Goal state after:
ι : Type u
c : ι → Type v
⊢ lift.{w, max v u} (prod fun i ↦ #(c i)) = prod fun i ↦ lift.{w, v} ((fun i ↦ #(c i)) i)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
⊢ ScottContinuousOn D (g ∘ f)

Tactic:
intro d hd₁ hd₂ hd₃ a ha
  have hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d) := by
    have := hf.monotone
    simp only [Monotone, DirectedOn, mem_image, exists_exists_and_eq_and, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂] at ⊢ this hd₃
    grind
  rw [Set.image_comp]
  exact hg (hD' hd₁) ⟨f hd₂.choose, by grind⟩ hd (hf hd₁ hd₂ hd₃ ha)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c ↦ Set.range ⇑c) c) a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
rw [← hf.2 c, ωSup_eq_of_isLUB hda]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
⊢ f y ≤ cSup c

Tactic:
· have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hc'
      apply hc'.2.resolve_left
      intro hc'
      exact lt_irrefl y (lt_of_lt_of_le hy' hc')

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

Goal state before:
pp: case inr
α : 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
this : Injective h
a : α
⊢ R a (h a)

Tactic:
simp only [h, Set.piecewise, g']

Goal state after:
case inr
α : 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
this : Injective h
a : α
⊢ R a (if a ∈ s then f a else invFun g a)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
by
  apply ωSup_le
  intro n
  induction n with
  | zero => exact h_x_le_a
  | succ n h_ind =>
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroClass M₀
inst✝ : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp [Prod.mul_def]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroClass M₀
inst✝ : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp [Prod.mul_def]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S✝ : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_14
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
⊢ fₗ (c • x) = c • fₗ x

Tactic:
induction c with
    | zero => simp
    | succ n ih => simp [add_smul]
    | pred n ih => simp [sub_smul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • mn.2 • (a + a') = mn • a + mn • a'

Tactic:
smul_add,

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • (mn.2 • a + mn.2 • a') = mn • a + mn • a'
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
x✝¹ : M
x✝ : M₂
⊢ ({ toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (((RingHom.id R) c • { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }) x✝¹) x✝

Tactic:
apply mul_smul

Goal state after: