mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
l : List M
⊢ f l.sum ≤ foldr max 0 (map f l)

Tactic:
by
  induction l with
  | nil => simpa using h0
  | cons hd tl IH =>
    simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
    exact (hadd _ _).trans (max_le_max le_rfl IH)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (foldl (argAux r) (some a✝) l✝) →
      m ∈ a✝ :: (l✝ ++ [a✝²])

Tactic:
cases _ : foldl _ _ _ <;> grind

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
wf : ↑m < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
rcases ofNat_surjective m with ⟨a, rfl⟩

Goal state after:
case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| n + 1

Tactic:
← ih,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({y ∈ range ↑(ofNat s n) | y ∈ s}) + 1
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) r₁ ++ [a :: l]

Tactic:
← ih,

Goal state after:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = sublists'Aux a r₁ r₂ ++ [a :: l]
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
⊢ #s ≤ #t + 1

Tactic:
set f : α → WithTop α := fun x => (t.filter fun y => x < y).min

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
⊢ #s ≤ #t + 1
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists' ↔ s <+ t

Tactic:
induction t generalizing s with

Goal state after:
case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = flatMap (fun l ↦ [l, a :: l]) r ++ flatMap (fun l ↦ [l, a :: l]) [l]

Tactic:
← ih,

Goal state after:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = sublistsAux a r ++ flatMap (fun l ↦ [l, a :: l]) [l]
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ i = s.min' hs

Tactic:
IsGLB,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGreatest (lowerBounds ↑s) i
⊢ i = s.min' hs
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ powersetCard n ↑l₁ ≤ powersetCard n ↑l₂

Tactic:
simp only [powersetCard_coe, coe_le]
    exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)

Tactic:
rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.powerset = {∅} ↔ s = ∅

Tactic:
← powerset_empty,

Goal state after:
α : Type u_1
s : Finset α
⊢ s.powerset = ∅.powerset ↔ s = ∅
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite

Tactic:
by
    refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩
    let u (i : {i | (s i).Nonempty}) : ⋃ i, s i := ⟨i.2.choose, mem_iUnion.2 ⟨i.1, i.2.choose_spec⟩⟩
    have u_inj : Function.Injective u := by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      ext
      refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
      rw [hij]
      exact hj.choose_spec
    have : Finite (⋃ i, s i) := h
    exact .of_injective u u_inj

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

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ↑(⨅ i ∈ s, f i) = ⨅ i ∈ s, ↑(f i)

Tactic:
refine le_antisymm (by simpa using fun _ ↦ biInf_le _) <|
    (le_iInf_iff.mpr fun i ↦ ?_).trans_eq (WithBot.coe_iInf _ (OrderBot.bddBelow _)).symm

Goal state after:
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
⊢ BddAbove (range fun i ↦ ⨆ j, f i j)

Tactic:
have ⟨a, h⟩ := H
  refine ⟨a ⊔ (sSup ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
  cases isEmpty_or_nonempty <| κ i
  · exact iSup_of_empty' (f i) ▸ le_sup_right
  exact ciSup_le fun j ↦ le_sup_of_le_left <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃₀ s).Infinite

Tactic:
rw [sUnion_eq_iUnion]
  have _ := hs.to_subtype
  exact infinite_iUnion Subtype.coe_injective

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

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = sSup ∅

Tactic:
cbiSup_of_not_bddAbove bdd

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ sSup ∅ = sSup ∅
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : ¬f j ≤ f i
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1

Tactic:
· exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
this : IsTop a
⊢ {a}.Subsingleton ∧ IsCofinal {a}

Tactic:
simpa [IsCofinal]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ico a a = 0

Tactic:
rw [Ico, Finset.Ico_self, Finset.empty_val]

Goal state after:
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 = Set.Ico (min a c) (max b d)

Tactic:
Set.Ico_union_Ico' hcb had

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Set.Ico (min a c) (max b 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 : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])

Tactic:
push_cast
    exact Set.uIcc_subset_uIcc_union_uIcc

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
g : ℕ → α
hg1 : ∀ m < n, Classical.choose ⋯ m = g m
hg2 : rk (g n) < rk (Classical.choose ⋯ n)
con : IsBadSeq r s g
⊢ False

Tactic:
refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
g : ℕ → α
hg1 : ∀ m < n, Classical.choose ⋯ m = g m
hg2 : rk (g n) < rk (Classical.choose ⋯ n)
con : IsBadSeq r s g
⊢ rk (g n) < Nat.find h
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa [reflTransGen_eq_self] using ReflTransGen.lift f h a b <| le_iff_reflTransGen_covBy.mp hab

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

Tactic:
by
  rw [← Function.Embedding.coe_subtype, ← prod_map]
  simp [attach_map_val]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
f : ι → M
⊢ (cons a s h).prod f = f a * ∏ x ∈ s, f x

Tactic:
rw [Finset.prod_cons h]

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 ι
h : s₁ ⊆ s₂
⊢ (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

Tactic:
rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]

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

Goal state before:
pp: α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]

Tactic:
red_iff_irreducible H1

Goal state after:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b ↔ a⁻¹ * b ∈ s

Tactic:
rw [leftRel_apply]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, hb h₂, mul_one]

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ (Submonoid.map e (closure ↑s)).FG

Tactic:
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆

Tactic:
H.range_subtype

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, H⁆ = ⁅H, H⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ (lift fun x ↦ 1) ((fun n ↦ n • of default) n) = n

Tactic:
map_zsmul,

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ n • (lift fun x ↦ 1) (of default) = n
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_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑(s' * s) ∈ S

Tactic:
apply SetLike.coe_mem

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 ↑0 = untopD 0 ↑0 * untopD 0 b

Tactic:
untopD_coe,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ 0 = 0 * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 ↑0 = untopD 0 a * untopD 0 ↑0

Tactic:
untopD_coe,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ 0 = untopD 0 a * 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 ↑(a✝¹ * a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝

Tactic:
untopD_coe,

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = untopD 0 ↑a✝¹ * untopD 0 ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = untopD 0 ↑a✝¹ * untopD 0 ↑a✝

Tactic:
untopD_coe,

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = a✝¹ * untopD 0 ↑a✝
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
inst✝ : Subsingleton M
mx : M
sx : ↥S
my : M
sy : ↥S
⊢ f.mk' mx sx = f.mk' my sy

Tactic:
exact congr(f.mk' $(Subsingleton.elim ..) $(Subsingleton.elim ..))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ ↑s₂ * r₁ = r₁ * ↑s₂

Tactic:
simp [mul_comm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]

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

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x a✝¹ a✝ : α
h : x * a✝¹ ≤ x * a✝
x0 : 0 < x
⊢ a✝¹ ≤ a✝

Tactic:
exact le_of_mul_le_mul_left h x0

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Tactic:
· by_cases hba : b ≤ a
    · exact (hb <| hba.trans <| le_succ _).trans (le_succ _)
    · exact succ_le_of_lt ((h.lt_of_not_ge hba).trans_le <| le_succ b)

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
⊢ a ∈ range succ

Tactic:
obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff_succ_eq.1 h

Goal state after:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a < f (a + 1)) → StrictMono f

Tactic:
simpa [Order.succ_eq_add_one] using strictMono_of_lt_succ (f := f)

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

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : ↑(y * z) = ↑1
x_z : ↑z = x.inv
x_y : ↑x = ↑y
⊢ x = default

Tactic:
natCast_inj,

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y * z = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑y
⊢ x = default
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ p a

Tactic:
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
      exact hp.1

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α ⊕ β)

Tactic:
by
  rcases exists_injective_nat α with ⟨f, hf⟩
  rcases exists_injective_nat β with ⟨g, hg⟩
  exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sumMap hg).countable

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
⊢ #({f ∈ piFinset s | f i = a}) = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0

Tactic:
split_ifs with h
  · rw [card_filter_piFinset_eq_of_mem _ _ h]
  · rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]

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

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (cons <$> f x✝ <*> Vector.traverse f w✝) =
    cons <$> ((fun {α} ↦ η.app α) ∘ f) x✝ <*> Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝

Tactic:
← ih,

Goal state after:
case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (cons <$> f x✝ <*> Vector.traverse f w✝) =
    cons <$> ((fun {α} ↦ η.app α) ∘ f) x✝ <*> (fun {α} ↦ η.app α) (Vector.traverse f w✝)
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'⟩
A : (f t ∩ f t').Nonempty
⊢ ⟨t, ht⟩ = ⟨t', ht'⟩

Tactic:
simp only [Subtype.mk.injEq]

Goal state after:
α : 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'⟩
A : (f t ∩ f t').Nonempty
⊢ t = t'
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i

Tactic:
exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩

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

Goal state before:
pp: case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ inr b

Tactic:
· change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)
        simp [toDual_le_toDual, inr_le_inr_iff]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c ((f.trans g.toRelEmbedding) a)
⊢ c ∈ Set.range ⇑(f.trans g.toRelEmbedding)

Tactic:
simp only [RelEmbedding.coe_trans, coe_coe_fn, comp_apply] at h ⊢
    rcases g.2 _ _ h with ⟨b, rfl⟩; have h := g.map_rel_iff.1 h
    rcases f.2 _ _ h with ⟨a', rfl⟩; exact ⟨a', rfl⟩

Goal state after: