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

Goal state before:
pp: case cons.inl
ι : 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✝ : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
hl_nonempty : [] ≠ []
hl : ∀ (a : α), a ∈ [] → p a
⊢ f [].prod ≤ (map f []).prod

Tactic:
simp at hl_nonempty

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

Tactic:
· exact Or.inr (Lex.left _ _ hji)

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

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = map (s.subtype.coprod t.subtype) ⊤

Tactic:
← mrange_inl_sup_mrange_inr,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = map (s.subtype.coprod t.subtype) (mrange (inl ↥s ↥t) ⊔ mrange (inr ↥s ↥t))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
rw [if_neg, if_neg]
      · exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
      · exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne
      · exact ne_of_apply_ne _ ‹f hd < f _›.ne

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = l.maximum

Tactic:
by
  induction l with
  | nil => contradiction
  | cons hd tl IH =>
    rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
· exact le_max_of_le_right (IH hl)

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ s.sup f = s.sup fun i ↦ a ⊓ f i

Tactic:
induction s using Finset.cons_induction with
  | empty => simp_rw [Finset.sup_empty, inf_bot_eq]
  | cons _ _ _ h => rw [sup_cons, sup_cons, inf_sup_left, h]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
x✝ : f b ≤ f c ∨ f c ≤ f b
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
cases le_total (f b) (f c) with

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x, t ↑x)

Tactic:
have : ∀ i : s, Finite (t i) := fun i => H i i.property

Goal state after:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ x, t ↑x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simp [iSup_of_empty']
  apply le_antisymm <| ciSup_le fun x ↦ sup_le_sup (le_ciSup Hf x) (le_ciSup Hg x)
  have := bbdAbove_range_sup Hf Hg
  exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)

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

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

Tactic:
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i, ↑i = sInf s

Tactic:
← sInf_range,

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ sInf (range fun i ↦ ↑i) = sInf s
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⋖ b ↔ a < b

Tactic:
by unfold CovBy; decide

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ a ∈ t, t \ {a} = s) → s ⋖ t

Tactic:
by rintro ⟨a, ha, rfl⟩; exact sdiff_singleton_covBy ha

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
wcovBy_iff_eq_or_covBy,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x = y ∨ x ⋖ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x

Tactic:
rw [mem_filter, mem_Ici, lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Tactic:
by
  tfae_have 1 → 2 := by
    refine fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩
    rw [← acc_transGen_iff] at h ⊢
    obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
    · rwa [h'] at h
    · exact h.inv h'
  tfae_have 2 → 3 := fun h => h.subset fun _ => TransGen.to_reflTransGen
  tfae_have 3 → 1 := by
    refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
    exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩
  tfae_finish

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite

Tactic:
by
  refine ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), ?_⟩
  rw [partiallyWellOrderedOn_iff_exists_lt]
  intro hs f hf
  by_contra! H
  refine infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)
  · obtain h | h | h := lt_trichotomy m n
    · refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _
    · exact h
    · refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _
  rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩ hmn
  obtain h | h := (ne_of_apply_ne _ hmn).lt_or_gt
  · exact H _ _ h
  · exact mt symm (H _ _ h)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
⊢ False

Tactic:
by_cases hn : n < g 0

Goal state after:
case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : n < g 0
⊢ False

case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : ¬n < g 0
⊢ False
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ ConjClasses.mk h = ConjClasses.mk g

Tactic:
ConjClasses.mk_eq_mk_iff_isConj,

Goal state after:
G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ IsConj h g
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s t : Multiset α
comm : {x | x ∈ s + t}.Pairwise Commute
⊢ (s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯

Tactic:
rcases s with ⟨⟩
  rcases t with ⟨⟩
  simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ Commute y (s.noncommProd f comm)

Tactic:
apply Multiset.noncommProd_commute
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
⊢ ↑(f x) = ↑(f y)

Tactic:
have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h

Goal state after:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
this :
  { val := ↑x, inv := ↑(f x), val_inv := ⋯, inv_val := ⋯ } = { val := ↑y, inv := ↑(f y), val_inv := ⋯, inv_val := ⋯ }
⊢ ↑(f x) = ↑(f y)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) =
            L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f g h i : ι → M
⊢ (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a

Tactic:
simp_rw [prod_mul_distrib, mul_mul_mul_comm]

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

Goal state before:
pp: case pos
ι : 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

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₁, one_mul]
    apply prod_eq_single_of_mem b h₂
    exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩

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 = f a * f b
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
⊢ x ∈ P → x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
intro hx₁
    by_cases hx₂ : x = 1
    · simp [hx₂]
    refine hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_
    simp only [Set.mem_ofPred_eq, and_imp] at ih
    by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y
    · exact mem_closure_of_mem hy₃
    rcases exists_lt_of_not_minimal ⟨hy₁, hy₂⟩ hy₃ with ⟨z, hz₁, hz₂, hz₃⟩
    rcases exists_mul_of_le hz₁.le with ⟨y, rfl⟩
    apply mul_mem
    · exact ih _ hz₂ hz₃ hz₁.le hz₁.not_ge
    apply ih
    · exact hP _ hz₂ _ hy₁
    · exact (one_lt_of_lt_mul_right hz₁).ne.symm
    · exact le_mul_self
    · rw [mul_le_iff_le_one_left']
      exact (one_lt_of_ne_one hz₃).not_ge

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✝ : Unique ι
f : ι → M
⊢ ∏ x, f x = f default

Tactic:
univ_unique,

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Unique ι
f : ι → M
⊢ ∏ x ∈ {default}, f x = f default
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ (map singleton s).sum = s

Tactic:
Multiset.sum_map_singleton

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ s = s
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ x₁ * of L2 * of L3 + x₂ * of L2 * of L3 = x₁ * (of L2 * of L3) + x₂ * (of L2 * of L3)

Tactic:
ih₁,

Goal state after:
case of.of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ x₁ * (of L2 * of L3) + x₂ * of L2 * of L3 = x₁ * (of L2 * of L3) + x₂ * (of L2 * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * y₁ * of L3 + x * y₂ * of L3 = x * (y₁ * of L3) + x * (y₂ * of L3)

Tactic:
ih₁,

Goal state after:
case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ * of L3) + x * y₂ * of L3 = x * (y₁ * of L3) + x * (y₂ * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * z₁ + x * y * z₂ = x * (y * z₁) + x * (y * z₂)

Tactic:
ih₁,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * (y * z₁) + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
ih : (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (of L1 * of L2) = -(lift ⇑f) (of L1) * (lift ⇑f) (of L2)

Tactic:
neg_mul

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
ih : (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (of L1 * of L2) = -((lift ⇑f) (of L1) * (lift ⇑f) (of L2))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
y : ↥S
⊢ f ↑(f.sec (f.mk' x y)).2 * (f.mk' x y * f ↑y) = f x * f ↑(f.sec (f.mk' x y)).2

Tactic:
f.mk'_spec,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
y : ↥S
⊢ f ↑(f.sec (f.mk' x y)).2 * f x = f x * f ↑(f.sec (f.mk' x y)).2
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ mk 1 1 = mk (↑a) a

Tactic:
mk_eq_mk_iff

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S) (1, 1) (↑a, a)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
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₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ r₁' • x /ₒ (s₁' * s) = r₂' • x /ₒ (s₂' * ⟨r₂ * ↑s, hs⟩)

Tactic:
rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ this]

Goal state after:
case c
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₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ (↑s₄' * r₃') • r₁' • x /ₒ ⟨↑s₄' * r₃' * ↑(s₁' * s), this⟩ =
    (s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩))
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
x : OreLocalization S X
⊢ 1 • x = x

Tactic:
cases x with | _ r s
   =>  _ 

Goal state after:
case c
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
⊢ 1 • (r /ₒ s) = r /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 1 = x

Tactic:
cases x with | _ r s
   =>  _ 

Goal state after:
case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 1 = r /ₒ s
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
s : M
hs : s ∈ ↑S
ht : g s ∈ T
x : M
⊢ ∃ a, (f.map hy k) a = k.mk' (g x) ⟨g s, ht⟩

Tactic:
use f.mk' x ⟨s, hs⟩

Goal state after:
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
s : M
hs : s ∈ ↑S
ht : g s ∈ T
x : M
⊢ (f.map hy k) (f.mk' x ⟨s, hs⟩) = k.mk' (g x) ⟨g s, ht⟩
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
x : OreLocalization S R
⊢ φ x = (universalMulHom f fS hf) x

Tactic:
cases x with | _ r s
   =>  _ 

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = (universalMulHom f fS hf) (r /ₒ s)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ oreNum (c • 1) s • r /ₒ oreDenom (c • 1) s = oreNum (c • 1) ⟨t * ↑s, ht⟩ • t • r /ₒ oreDenom (c • 1) ⟨t * ↑s, ht⟩

Tactic:
by
    rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
x : α
⊢ x - 1 ⋖ x

Tactic:
by
  rw [← pred_eq_sub_one]
  exact pred_covBy x

Goal state after: