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

Goal state before:
pp: case mp
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f → ∃ b ∈ s, a ≤ f b

pp: case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Tactic:
· induction s using cons_induction with
    | empty => exact (absurd · (not_le_of_gt ha))
    | cons c t hc ih =>
      rw [sup_cons, le_sup_iff]
      exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩

Goal state after:
case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < max (f c) (t.sup f) → ∃ b ∈ cons c t hc, a < f b

Tactic:
lt_sup_iff

Goal state after:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mp
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f → ∃ b ∈ s, a < f b

pp: case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f

Tactic:
· induction s using cons_induction with
    | empty => exact (absurd · not_lt_bot)
    | cons c t hc ih =>
      rw [sup_cons, lt_sup_iff]
      exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩

Goal state after:
case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
by
  simp_rw [← @WithBot.coe_le_coe α, coe_sup', Finset.sup_le_iff]; rfl

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

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
c : ι
⊢ ∃ i ∈ {c}, {c}.sup' ⋯ f = f i

Tactic:
exact ⟨c, mem_singleton_self c, rfl⟩

Goal state after:
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
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
⊢ {i | (s i).Nonempty}.Finite

Tactic:
have : Finite (⋃ i, s i) := h

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
this : Finite ↑(⋃ i, s i)
⊢ {i | (s i).Nonempty}.Finite
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
WithTop.sInf_empty

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : IsEmpty ι
inst✝ : InfSet α
f : ι → WithTop α
⊢ ⊤ = ⊤
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ range f, t i

Tactic:
rw [biUnion_range, mem_iUnion]

Goal state after:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ⨆ c, f (b, c) ≤ c

Tactic:
ciSup_le_iff (h₂ b)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ∀ (i : γ), f (b, i) ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ⨅ x ∈ l, f x ∈ map f l

Tactic:
by
  classical
  simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

pp: case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Tactic:
· exact Or.inr h3

Goal state after:
case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b
Module: Mathlib.Order.Interval.Finset.Defs

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

Tactic:
by rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
by
  cases eq_empty_or_nonempty s with
  | inl h => subst h
             simp only [or_true, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s

Tactic:
by
  classical
  cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
⊢ s.Nonempty

Tactic:
by_contra contra

Goal state after:
s : Set ℕ
h : 0 < sInf s
contra : ¬s.Nonempty
⊢ False
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a

Tactic:
rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
a : α
b : ↑(Set.Iic a)
⊢ ↑b ∈ Set.Iic a

Tactic:
exact b.2

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

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

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

Tactic:
· rw [Icc_eq_cons_Ico h, card_cons]
    exact (Nat.add_sub_cancel _ _).symm

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
h : ¬hs.min ⋯ = a
⊢ False

Tactic:
exact (hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha))
    (hs.min_mem (nonempty_of_mem ha)) h)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
⊢ hs.min ⋯ = a

Tactic:
by_contra h
  exact (hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha))
    (hs.min_mem (nonempty_of_mem ha)) h)

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ x.orbit = MulAction.orbit G (φ x)

Tactic:
conv_lhs => rw [← hφ x]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ orbit (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
· exact .single <| wcovBy_of_le_of_le hxy hxy'

Goal state after:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: 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)
n : ℕ
x : α
hn : n < g 0
hx : x ∈ f n
⊢ x ∈ s

pp: 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)
n : ℕ
x : α
hn : ¬n < g 0
hx : x ∈ (f (g (n - g 0))).tail
⊢ x ∈ s

Tactic:
exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M

Tactic:
exact mul_mem_center ha (inv_mem_center hb)

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
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:
convert! hh

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h = g * h * g⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : G
hx : x ∈ S i
⊢ ∃ (h : x ∈ ⨆ i, S i), C x h

pp: case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h

pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
· exact ⟨_, hp i _ hx⟩

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h

case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Normal
⊢ (⨆ i ∈ s, H i).Normal

Tactic:
rw [← iSup_subtype'']
  have : ∀ i : s, (H i).Normal := fun i ↦ h i i.property
  apply iSup_normal

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g ∈ normalizer ↑H

Tactic:
rw [← (normalizer H : Subgroup G).inv_mem_iff]
  simp only [Subgroup.ext_iff, mem_pointwise_smul_iff_inv_smul_mem,
    ← ConjAct.toConjAct_inv, ConjAct.toConjAct_smul, mem_normalizer_iff, inv_inv, Iff.comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.negSucc n) (x ^ Int.negSucc n)

Tactic:
by simpa only [zpow_negSucc] using c.inv (c.pow _ h)

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
⊢ ((∏ x ∈ s, f x) * ∏ x ∈ s, g x) * ((∏ x ∈ s, h x) * ∏ x ∈ s, i x) =
    ((∏ x ∈ s, f x) * ∏ x ∈ s, h x) * ((∏ x ∈ s, g x) * ∏ x ∈ s, i x)

Tactic:
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

Tactic:
ha h₁,

Goal state after:
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 = 1 * f b
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:
ha h₁,

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG

Tactic:
rcases hP with ⟨s, rfl⟩

Goal state after:
M : Type u_1
inst✝ : Monoid M
Q : Submonoid M
hQ : Q.FG
s : Finset M
⊢ (closure ↑s ⊔ Q).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0

Tactic:
rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)
⊢ ∏ x ∈ range (n + (m + 1)), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range (m + 1), f (n + x)

Tactic:
rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P Q : Subgroup G
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG

Tactic:
rcases hP with ⟨s, rfl⟩

Goal state after:
G : Type u_3
inst✝ : Group G
Q : Subgroup G
hQ : Q.FG
s : Finset G
⊢ (closure ↑s ⊔ Q).FG
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
neg_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
neg_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= fun x ↦ f x >>= g) = -pure x >>= fun x ↦ f x >>= g

Tactic:
neg_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= fun x ↦ f x >>= g) = -(pure x >>= fun x ↦ f x >>= g)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ 0 <*> y = (fun b a ↦ (a, b)) <$> y <*> 0

Tactic:
zero_seq,

Goal state after:
case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ 0 = (fun b a ↦ (a, b)) <$> y <*> 0
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
a : GrothendieckGroup M
⊢ a⁻¹ * a = 1

Tactic:
cases a using ind
    rw [inv_mk, mk_eq_monoidOf_mk', ← Submonoid.LocalizationMap.mk'_mul]
    convert! Submonoid.LocalizationMap.mk'_self' _ _
    rw [mul_comm, Submonoid.coe_mul]

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

Goal state before:
pp: case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))

Tactic:
· simp [mul_pow, pow_succ c, mul_assoc, hab]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0

Tactic:
cases x <;> cases n

Goal state after:
case top.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊤ ^ 0 = ⊤ ↔ ⊤ = ⊤ ∧ 0 ≠ 0

case top.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n✝ : ℕ
⊢ ⊤ ^ (n✝ + 1) = ⊤ ↔ ⊤ = ⊤ ∧ n✝ + 1 ≠ 0

case coe.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
⊢ ↑a✝ ^ 0 = ⊤ ↔ ↑a✝ = ⊤ ∧ 0 ≠ 0

case coe.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
n✝ : ℕ
⊢ ↑a✝ ^ (n✝ + 1) = ⊤ ↔ ↑a✝ = ⊤ ∧ n✝ + 1 ≠ 0
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
inst✝⁴ : SMul Rᵐᵒᵖ M
inst✝³ : SMul Rᵐᵒᵖ X
inst✝² : IsScalarTower Rᵐᵒᵖ M M
inst✝¹ : IsScalarTower Rᵐᵒᵖ M X
inst✝ : IsCentralScalar R M
r : R
x : OreLocalization S X
⊢ MulOpposite.op r • x = r • x

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_smul]

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

Goal state before:
pp: case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

pp: case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝ * b) = unbotD 0 ↑a✝ * unbotD 0 b

Tactic:
· rw [bot_mul hb, unbotD_bot, zero_mul]

Goal state after:
case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝ * b) = unbotD 0 ↑a✝ * unbotD 0 b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : ↑(succ a) = ↑a
⊢ False

Tactic:
rw [coe_succ_of_mem nh] at h

Goal state after:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : succ ↑a = ↑a
⊢ False