mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Tactic:
← inv_subset_inv,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s⁻¹⁻¹ ⊆ t⁻¹ ↔ s ⊆ t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
| (fun x ↦ (g x)⁻¹) '' s

Tactic:
← image_inv_of_apply_inv_eq H

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
| f '' s⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, image2 f s (t i j)

Tactic:
by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
inv_mem : ∀ (x : G), x ∈ s → x⁻¹ ∈ s
a✝ b✝ : G
hx : a✝ ∈ s
hy : b✝ ∈ s
⊢ a✝ * b✝ ∈ s

Tactic:
simpa using hs _ hx _ (inv_mem _ hy)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ map f (H ⊓ K) = ⊥

Tactic:
disjoint_iff.mp h,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ map f ⊥ = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ K : Subgroup G
⊢ H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Tactic:
by
  simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
A : Type u_4
inst✝² : AddGroup A
H✝ : Type u_5
inst✝¹ : Group H✝
H : Type u_6
inst✝ : Group H
f : G ≃* H
sg1 sg2 : Subgroup G
h :
  { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤
    { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2
⊢ sg1 ≤ sg2

Tactic:
simpa [Subgroup.map_map] using
      Subgroup.map_mono (f := (f.symm : H →* G)) h

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⋃ i, ↑(S i), ∀ b ∈ ⋃ i, ↑(S i), a * b = b * a

Tactic:
Set.mem_iUnion,

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : G), (∃ i, a ∈ ↑(S i)) → ∀ (b : G), (∃ i, b ∈ ↑(S i)) → a * b = b * a
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ map f (H ⊓ K) = ⊥

Tactic:
disjoint_iff.mp h,

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ map f ⊥ = ⊥
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) = ⊤.prod ⊥

Tactic:
by simpa only [mrange_eq_map] using map_inl ⊤

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b n).div2 = n

Tactic:
by
  rw [div2_val, bit_div_two]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Encodable α
e : β ≃ α
n : ℕ
⊢ (decode n).bind (some ∘ ⇑e.symm) = Option.map (⇑e.symm) (decode n)

Tactic:
rw [Option.map_eq_bind]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
exact (Classical.choose_spec (hf p a)).1

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: ⊢ AddSubgroup.closure {1} = ⊤

Tactic:
ext
  simp [AddSubgroup.mem_closure_singleton]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H

Tactic:
exact H.one_mem

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective f

Tactic:
constructor
  · intro fs d
    rcases fs (FreeMonoid.of d) with ⟨b, hb⟩
    induction b using FreeMonoid.inductionOn' with
    | one =>
      have H := congr_arg length hb
      simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
    | of_mul head _ _ =>
      simp only [map_mul, map_of] at hb
      use head
      have H := congr_arg length hb
      simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
      rw [H, mul_one] at hb
      exact FreeMonoid.of_injective hb
  intro fs d
  induction d using FreeMonoid.inductionOn' with
  | one => use 1; rfl
  | of_mul head tail ih =>
    specialize fs head
    rcases fs with ⟨a, rfl⟩
    rcases ih with ⟨b, rfl⟩
    use FreeMonoid.of a * b
    rfl

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⋃ i, ↑(S i), ∀ b ∈ ⋃ i, ↑(S i), a * b = b * a

Tactic:
Set.mem_iUnion,

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M), (∃ i, a ∈ ↑(S i)) → ∀ (b : M), (∃ i, b ∈ ↑(S i)) → a * b = b * a
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
cases n with
    | zero =>
      refine ⟨none, ?_, encode_none⟩
      rw [decode_option_zero, Option.mem_def]
    | succ n =>
      refine ⟨some (ofNat α n), ?_, ?_⟩
      · rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
      rw [encode_some, encode_ofNat]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : ↑x + 1 ≤ a
⊢ ↑x + (a - (↑x + 1)) + 1 ∈ s

Tactic:
Nat.add_right_comm,

Goal state after:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : ↑x + 1 ≤ a
⊢ ↑x + 1 + (a - (↑x + 1)) ∈ s
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ z = y

Tactic:
exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⊔ b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
rw [comp_apply, map_sup, map_sup]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g a) ⊔ f (g b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case empty
α : Type u_2
inst✝ : LinearOrder α
a✝ : α
H : ∅.max = ↑a✝
⊢ a✝ ∈ ∅

Tactic:
cases H

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ ↑((s.erase x).max' s0) ≠ ↑x

Tactic:
exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
⊢ {x ∈ powersetCard n t | s ⊆ x} = image (fun x ↦ x ∪ s) (powersetCard (n - #s) (t \ s))

Tactic:
by
  ext x
  simp only [mem_filter, mem_powersetCard, mem_image]
  constructor
  · intro ⟨⟨hxt, hxn⟩, hsx⟩
    exact ⟨x \ s, ⟨fun y hy => mem_sdiff.mpr ⟨hxt (mem_sdiff.mp hy).1, (mem_sdiff.mp hy).2⟩,
           by rw [card_sdiff_of_subset hsx, hxn]⟩, sdiff_union_of_subset hsx⟩
  · rintro ⟨y, ⟨hyt, hyn⟩, rfl⟩
    refine ⟨⟨union_subset (hyt.trans sdiff_subset) hst, ?_⟩, subset_union_right⟩
    rw [card_union_of_disjoint (disjoint_of_subset_left hyt disjoint_sdiff_self_left), hyn]
    lia

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t

Tactic:
h₀.eq (subset_union_left hi) (subset_union_right hj)
      (not_disjoint_iff.2 ⟨a, hai, haj⟩)

Goal state after:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ j ∈ t
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:
by
  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.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
← sup_congr (Eq.refl s) hfinvs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = s.sup (f ∘ invFunOn f (f ⁻¹' ↑s))
Module: Mathlib.Order.Lattice.Nat

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

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at contra

Goal state after:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)

Tactic:
← sup_iSup_nat_succ

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ i, ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
H K : Submonoid M
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
rw [closure_eq, closure_eq]

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
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
rw [Ico_eq_cons_Ioo h, card_cons]

Goal state after:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s

Tactic:
rw [closure_inv, mem_inv]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
⊢ ↑(ConjAct.ofConjAct ↑u) ∈ Submonoid.centralizer {↑x}

Tactic:
by
          rintro x ⟨rfl⟩
          have : (u : ConjAct Mˣ) • x = x := u.2
          rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this

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

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x y : G
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
ihx : C x
ihy : C y
⊢ C (x * y)

Tactic:
exact mul x y ihx ihy

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
rw [closure_eq, closure_eq]

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

Goal state before:
pp: case mul
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x✝ y✝ : G
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : ∀ {x : X}, x ∈ t → x✝ • x ∈ t
h₂ : ∀ {x : X}, x ∈ t → y✝ • x ∈ t
x : X
hx : x ∈ t
⊢ x✝ • y✝ • x ∈ t

Tactic:
exact h₁ (h₂ hx)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
x y a b : α
h : r a b
ha : f a = f x
hb : f b = f y
⊢ r x y

Tactic:
replace ha := hf ha
    replace hb := hf hb
    exact trans (symm ha) (trans h hb)

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

Goal state before:
pp: α : Type u
L L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False

Tactic:
rcases h with - | ⟨L₁, L₂⟩

Goal state after:
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False
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
⊢ ∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x

Tactic:
rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]

Goal state after:
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)

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

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:
case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ Con.liftOn 1 ⇑f ⋯ = 1

Tactic:
rw [← f.map_one]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ Con.liftOn 1 ⇑f ⋯ = f 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁

Tactic:
cases H

Goal state after:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail
α : Type u
L₁ L₂ b✝ c✝ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b✝
h₂₃ : Step b✝ c✝
ih : ∃ n, L₁.length = b✝.length + 2 * n
⊢ ∃ n, L₁.length = c✝.length + 2 * n

Tactic:
rcases ih with ⟨n, eq⟩
    exists 1 + n
    simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

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

Goal state before:
pp: α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁ L₂ : List (α × Bool)
H : Red.Step L₁ L₂
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) L₁) (List.map (fun x ↦ (f x.1, x.2)) L₂)

Tactic:
cases H

Goal state after:
case not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝))
    (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ L₂✝))
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
ι : Type u_3
s : Set ι
hs : s.Finite
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
by
  simpa using biSup_finset hs.toFinset P (by simpa)

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

pp: case mpr.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S

Tactic:
· rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
      exact Submonoid.subset_closure

Goal state after:
case mpr.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG

Tactic:
rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]

Goal state after:
H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Set ι
hs : s.Finite
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
by
  simpa using biSup_finset hs.toFinset P (by simpa)

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst✝¹ : G'.Normal
inst✝ : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
x : G ⧸ G'
⊢ (map H' G' ↑e.symm ⋯) ((map G' H' ↑e ⋯) x) = x

Tactic:
map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
        (he ▸ (G'.map_equiv_eq_comap_symm e).le)

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst✝¹ : G'.Normal
inst✝ : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
x : G ⧸ G'
⊢ (map G' G' ((↑e.symm).comp ↑e) ⋯) x = x
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs : s ∈ ⊥
h : x✝¹ * ↑⟨s, hs⟩ = x✝ * ↑⟨s, hs⟩
⊢ ↑⟨s, hs⟩ * x✝¹ = ↑⟨s, hs⟩ * x✝

Tactic:
rw [Submonoid.mem_bot] at hs

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
h : x✝¹ * ↑⟨s, hs✝⟩ = x✝ * ↑⟨s, hs✝⟩
⊢ ↑⟨s, hs✝⟩ * x✝¹ = ↑⟨s, hs✝⟩ * x✝
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs : s ∈ ⊥
⊢ ↑⟨s, hs⟩ * x✝ = x✝ * ↑⟨s, hs⟩

Tactic:
rw [Submonoid.mem_bot] at hs

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
⊢ ↑⟨s, hs✝⟩ * x✝ = x✝ * ↑⟨s, hs✝⟩
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i = (∏ i ∈ s \ t, f i) * ∏ i ∈ t, f i

Tactic:
← prod_union disjoint_sdiff_self_left,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ t \ s ∪ s, f x = (∏ i ∈ s \ t, f i) * ∏ i ∈ t, f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ t \ s ∪ s, f x = (∏ i ∈ s \ t, f i) * ∏ i ∈ t, f i

Tactic:
← prod_union disjoint_sdiff_self_left,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ t \ s ∪ s, f x = ∏ x ∈ s \ t ∪ t, f x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : ∃ a_1 ∈ base, ∃ c, c * a_1 * c⁻¹ = a
⊢ a ∈ base

Tactic:
rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
c : G
hc : c ∈ H₁
e : G
he : e ∈ H₂
d : G
⊢ d * ⁅c, e⁆ * d⁻¹ ∈ base
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
z x y : FreeAbelianGroup T
hx : (lift fun x ↦ 1) x • of default = x
hy : (lift fun x ↦ 1) y • of default = y
⊢ (lift fun x ↦ 1) x • of default + (lift fun x ↦ 1) y • of default = x + y

Tactic:
rw [hx, hy]

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

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

Tactic:
smul'_char _ _ _ _ _ _ h₁

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
⊢ r₁' • r₁ /ₒ (s₁' * s) = smul' r s (r₂ • r₁) ⟨r₂ * ↑s', hs⟩