mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.inr
α : 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 : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (b : β) (i : γ), f (b, i) ≤ c

Tactic:
simp [Prod.forall]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ x ∈ s, f x ∈ map f s

Tactic:
classical
  simpa using s.toFinset.ciSup_mem_image f (by simpa using h)

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

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Tactic:
rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩

Goal state after:
case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
this : Nonempty (Exists p)
x✝ : Exists p
i : ι
hi : p i
⊢ f ⋯ ∈ upperBounds (⋃ i_1, range fun x ↦ f ⋯)

Tactic:
rintro _ ⟨_, ⟨j, rfl⟩, ⟨hj, rfl⟩⟩

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
this : Nonempty (Exists p)
x✝ : Exists p
i : ι
hi : p i
j : ι
hj : p j
⊢ (fun x ↦ f ⋯) hj ≤ f ⋯
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
by_cases h₁ : x.1 ∈ s₁

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
⊢ a i ⩿ b i

Tactic:
classical
  refine ⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩
  have hcb : Function.update a i ci ≤ b := by simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j
  refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)
  simp [le_update_iff, h₂.not_ge]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithTop α
⊢ a ⋖ ⊤ ↔ ∃ b, IsMax b ∧ a = ↑b

Tactic:
cases a with

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ P x ∧ Q x) x ↔ Minimal P x ∧ Q x

Tactic:
simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]
  exact fun h ↦ hPQ h.prop

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
⊢ MinimalFor Q f i

Tactic:
refine ⟨h.prop, fun j hj hle ↦ ?_⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
⊢ f i ≤ f j
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
⊢ f i ≤ f j

Tactic:
by_contra

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
this : ¬f i ≤ f j
⊢ False
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
⊢ MaximalFor Q f i

Tactic:
refine ⟨h.prop, fun j hj hle ↦ ?_⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
⊢ f j ≤ f i
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
⊢ f j ≤ f i

Tactic:
by_contra

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
this : ¬f j ≤ f i
⊢ False
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ f y ≤ f x → f x ≤ f y

Tactic:
f.le_iff_le

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ y ≤ x → x ≤ y
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ (Finset.Ioc a a).val = 0

Tactic:
Finset.Ioc_self,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ ∅.val = 0
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 ∈ finsetIcc a b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b

Tactic:
mem_Icc,

Goal state after:
α : 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 : α
⊢ (a ≤ x ∧ x ≤ b) ∧ ¬b ≤ x ↔ a ≤ x ∧ x < 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 ∈ finsetIcc a b ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
α : 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 : α
⊢ (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ↔ a < x ∧ x ≤ 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 ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b

Tactic:
mem_Icc,

Goal state after:
α : 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 : α
⊢ (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ finsetIcc a b ∧ x ≠ b ↔ a ≤ x ∧ x < b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ x ≤ b) ∧ x ≠ b ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ finsetIcc a b ∧ a ≠ x ↔ a < x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ x ≤ b) ∧ a ≠ x ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ finsetIcc a b ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ x ≤ b) ∧ a ≠ x ∧ x ≠ b ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ x ∈ Icc a ⊤ ↔ a ≤ x

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ a ≤ x ∧ x ≤ ⊤ ↔ a ≤ x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Icc (f a) (f b) ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f a ≤ f x ∧ f x ≤ f b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ a ≤ x ∧ f x ≤ f b ↔ a ≤ x ∧ x ≤ b

Tactic:
f.le_iff_le

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ a < x ∧ f x ≤ f b ↔ a < x ∧ x ≤ b

Tactic:
f.le_iff_le

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ x.1 ≤ b.1) ∧ a.2 ≤ x.2 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑x ∈ Icc ↑a ↑b ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_Icc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑a ≤ ↑x ∧ ↑x ≤ ↑b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
w✝¹ w✝ : ℕ
hle : w✝¹ < w✝
hr : r ((Function.surjInv hf ∘ seq) w✝¹) ((Function.surjInv hf ∘ seq) w✝)
⊢ s (seq w✝¹) (seq w✝)

Tactic:
by simpa [Function.surjInv_eq] using f.map_rel hr

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b

Tactic:
simpa only [H, and_true] using @hf

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a

Tactic:
simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

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 α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ f (g⁻¹ • a) = f a

Tactic:
simp +instances [f, orbitRel, Quotient.eq']

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Tactic:
simp_rw [mem_uIcc]
  exact Set.eq_of_mem_uIcc_of_mem_uIcc

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ g = y

Tactic:
hy.eq_of_right_mem_center hg

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ g = g
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g * n * g⁻¹ ∈ H

Tactic:
rw [← h g, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, MulAut.smul_def,
    MulAut.conj_apply, inv_inv, mul_assoc, mul_assoc, inv_mul_cancel, mul_one,
    ← mul_assoc, inv_mul_cancel, one_mul]

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H

Tactic:
exact hn

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)

Tactic:
← Finset.toLeft_disjSum_toRight (u := s),

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ ∏ x ∈ s.toLeft.disjSum s.toRight, f x =
    (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x)) *
      ∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x)
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
⊢ (c.lift f H).comp c.mk' = f

Tactic:
ext; rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((rightRel s) x y)

Tactic:
rw [rightRel_eq]

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((fun x y ↦ y * x⁻¹ ∈ s) x y)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refl
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∃ n, L₁.length = L₁.length + 2 * n

Tactic:
exact ⟨0, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ (rightRel s) g g

Tactic:
exact Quotient.exact' rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ (leftRel s) g g

Tactic:
exact Quotient.exact' rfl

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℤ
⊢ (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) x) = x

Tactic:
induction x with
    | zero => simp
    | succ x hx => simpa [zpow_add_one] using hx
    | pred x hx => simpa [zpow_sub_one, ← sub_eq_add_neg] using hx

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : id <$> of x = of x
⊢ id <$> (of x)⁻¹ = (of x)⁻¹

Tactic:
rw [map_inv, ih]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
H : g b = 1
⊢ False

Tactic:
by rw [H] at h₂; simp at h₂

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P : Submonoid M
x✝ : ∃ S, closure S = P ∧ S.Finite
S : Set M
hS : closure S = P
hf : S.Finite
⊢ closure ↑hf.toFinset = P

Tactic:
simp [hS]

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

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

Tactic:
rw [range_add_one, prod_insert notMem_range_self]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
bM : Finset M
hbM : closure ↑bM = P
bN : Finset N
hbN : closure ↑bN = Q
⊢ closure (↑bM ×ˢ {1} ∪ {1} ×ˢ ↑bN) = P.prod Q

Tactic:
simp [closure_union, hbM, hbN]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P : Subgroup G
x✝ : ∃ S, closure S = P ∧ S.Finite
S : Set G
hS : closure S = P
hf : S.Finite
⊢ closure ↑hf.toFinset = P

Tactic:
simp [hS]

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
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
⊢ ∀ x ∈ s, f x = 1

Tactic:
by
  intro x hx
  classical
    by_cases h : x = a
    · rw [h]
      rw [h] at hx
      rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
      exact hp
    · exact h1 x hx h

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ ∏ x ∈ s, ∏ i ∈ t' x, f i = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))

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

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0

Tactic:
apply sum_range_induction
  case base => apply tsub_eq_of_eq_add; rw [zero_add]
  case step =>
    intro n _
    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : Prod.mk <$> x₁ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁
ih2 : Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₂
⊢ (Prod.mk <$> x₁ <*> y) + (Prod.mk <$> x₂ <*> y) = (fun b a ↦ (a, b)) <$> y <*> x₁ + x₂

Tactic:
seq_add,

Goal state after:
case add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : Prod.mk <$> x₁ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁
ih2 : Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₂
⊢ (Prod.mk <$> x₁ <*> y) + (Prod.mk <$> x₂ <*> y) =
    ((fun b a ↦ (a, b)) <$> y <*> x₁) + ((fun b a ↦ (a, b)) <$> y <*> x₂)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer ↑⁅H₁, H₂⁆

Tactic:
by
  rw [commutator_comm]
  apply normalizer_commutator_ge_left

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ IsMulCommutative (G ⧸ N)

Tactic:
apply Function.Surjective.mul_comm (f := φ) _ hH

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ⋯
⊢ Function.Surjective ⇑φ
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * r₁ * r * r₂ = r₁' * ↑t * r * r₂

Tactic:
hr₁

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r * r₂ = r₁' * ↑t * r * r₂
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r' * r₂ = ↑t' * r₁ * r' * r₂

Tactic:
hr₁

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r' * r₂ = r₁' * ↑t * r' * r₂