mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a * a = a

Tactic:
h.eq

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a = a
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsIdempotentElem a
n : ℕ
hn : n ≠ 0
⊢ a ^ n = a

Tactic:
obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
  exact h.pow_succ_eq _

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ (fun x ↦ a • x) '' s / (fun x ↦ b • x) '' t = (fun x ↦ (a / b) • x) '' (s / t)

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ (fun a_1 ↦ a * a_1) '' s / (fun a ↦ b * a) '' t = (fun a_1 ↦ a / b * a_1) '' (s / t)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons_cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂✝ → 1 ≤ a_1
⊢ (a :: l₁✝).prod ≤ (a :: l₂✝).prod

Tactic:
simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x

Tactic:
iSup_eq_closure

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn none (some a) fun c ↦ if r a c then some a else some c
hf : tl = [] ∧ o = none
⊢ ¬r b m

Tactic:
simp_all [hf.1, hf.2, hr₀.irrefl _]

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✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
by
    refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
    rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_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✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this : Lattice { x // P x } := Subtype.lattice Psup Pinf
⊢ ∀ (a b : { x // P x }),
    (SupHom.subtypeVal Psup).toFun (a ⊓ b) = (SupHom.subtypeVal Psup).toFun a ⊓ (SupHom.subtypeVal Psup).toFun b

Tactic:
by simp [Subtype.coe_inf Pinf]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max

Tactic:
by
  rw [max_eq_sup_withBot, sup_image]
  exact congr_fun WithBot.map_id _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max

Tactic:
by
  rw [max_eq_sup_withBot, sup_image]
  exact congr_fun WithBot.map_id _

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

Goal state before:
pp: α : Type u
l : List α
⊢ map pure l <+ l.sublists

Tactic:
induction l using reverseRecOn <;> simp only [map, map_append, sublists_concat]
  · simp only [sublists_nil, sublist_cons_self]
  case append_singleton l a ih =>
    exact ((append_sublist_append_left _).2 <|
              singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
          ((append_sublist_append_right _).2 ih)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s

Tactic:
unfold sublistsLenAux

Goal state after:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s

Tactic:
unfold sublistsLenAux

Goal state after:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) l (g ∘ f) (sublistsLenAux n l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ cons a) r)) ++ s
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')

pp: case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
· refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_
    · convert! le_iSup₂ (α := α) i hi.1; rfl
    · convert! le_iSup₂ (α := α) i hj.1; rfl

Goal state after:
case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ ⊥ = a \ ∅.inf f

Tactic:
inf_empty,

Goal state after:
case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ ⊥ = a \ ⊤
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
h : s.Nonempty
f : β → α
⊢ ↑(s.sup f) = s.sup (WithBot.some ∘ f)

Tactic:
simp only [← sup'_eq_sup h, coe_sup' h]

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

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Tactic:
have := map_finset_sup f hs.toFinset g

Goal state after:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (hs.toFinset.sup g) = hs.toFinset.sup (⇑f ∘ g)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t : Finset ι
⊢ ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
by
  suffices ∀ st : Finset ι, BddAbove <| .range fun x ↦ ⨆ (_ : x ∈ st), f x by
    simp [ciSup_or', ciSup_sup_eq, this]
  refine fun st ↦ ⟨st.sup f, fun a ⟨i, ha⟩ ↦ ha ▸ ?_⟩
  by_cases h : i ∈ st <;>
    simp [h, le_sup]

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
rcases h2.eq_or_lt with (h2 | h2)

Goal state after:
case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

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

Goal state before:
pp: case e'_4
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ insert a (s \ {a})

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s

Tactic:
simp [ha]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (s.sigma t).sup f = s.sup fun i ↦ (t i).sup fun b ↦ f ⟨i, b⟩

Tactic:
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a), a ∈ s → b ∈ t a → f ⟨a, b⟩ ≤ s.sup fun i ↦ (t i).sup fun b ↦ f ⟨i, b⟩) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f ⟨b, b_1⟩ ≤ (s.sigma t).sup f
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ¬BddAbove s
⊢ (if h : ∃ n, ∀ a ∈ s, a ≤ n then Nat.find h else 0) = Nat.find ⋯

Tactic:
rw [dif_neg]

Goal state after:
s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find ⋯

case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
  · intro n ih m hm
    rcases hm.eq_or_lt with rfl | hm
    · exact step n ih
    · exact ih m hm
  · rintro ⟨b, hb⟩
    rcases base with ⟨n, hn⟩
    specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
    all_goals lia

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2

Tactic:
exact (RelEmbedding.ofMonotone _ h1).swap

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α

Tactic:
by
  rw [wellQuasiOrderedLE_iff, and_iff_left_iff_imp]
  exact fun _ s hs ↦ hs.subsingleton.finite

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
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
by_contra! H

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ False
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
rw [partiallyWellOrderedOn_iff_exists_monotone_subseq]
    intro f hf
    simp only [mem_pi, mem_univ, forall_const] at hf
    simpa only [Finset.mem_univ, true_imp_iff] using! this Finset.univ f hf

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • ↑x • y = ↑x • g • y

Tactic:
smul_eq_mul,

Goal state after:
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • (↑x * y) = ↑x * g • y
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mp
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
hb : (fun m ↦ m • a) g ∈ U
hab : f ((fun m ↦ m • a) g) = f a
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U

Tactic:
rw [Set.mem_iUnion]

Goal state after:
case mp
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
hb : (fun m ↦ m • a) g ∈ U
hab : f ((fun m ↦ m • a) g) = f a
⊢ ∃ i, a ∈ (fun x ↦ i • x) '' U
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
h : ⊤ ⊆ S.centralizer
x✝¹ : M
hx : x✝¹ ∈ S
x✝ : M
⊢ x✝ * x✝¹ = x✝¹ * x✝

Tactic:
rw [h trivial _ hx]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

Tactic:
by
  refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
  · refine
      closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx
    rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
  · simp only [true_and, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]

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

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 (hd :: tl) = (hd :: tl).prod

Tactic:
rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 l = l.prod

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

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

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

Tactic:
iSup_eq_closure

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(H ⊔ N) = ↑H * ↑N

Tactic:
rw [sup_eq_closure_mul]
  refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
  induction hx using closure_induction'' with
  | one => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
  | mem _ hx => exact hx
  | inv_mem x hx =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))
  | mul x' x' _ _ hx hx' =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    obtain ⟨x', hx', y', hy', rfl⟩ := hx'
    refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
    · exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
    · simp only [mul_assoc, mul_inv_cancel_left]

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

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ l, p x
⊢ p l.prod

Tactic:
exact l.prod_induction p hom unit base

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s)).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
by
  simp only [← cons_eq_insert _ _ ha, noncommProd_cons']

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
x y : (i : ι) → α i
hxy : piSetoid x y
i : ι
⊢ Quotient.mk'' (x i) = Quotient.mk'' (y i)

Tactic:
simpa [Quotient.eq] using hxy i

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
a : α
⊢ (lift f) (of a) = f a

Tactic:
simp only [lift_apply_of]

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.biUnion t with f x ≠ 1, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
← this,

Goal state after:
ι : 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.biUnion t', f x = ∏ x ∈ s, ∏ i ∈ t x, f i
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a✝ : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ g ((lift f) (of a)) = g (f a)

Tactic:
simp only [lift_apply_of]

Goal state after:
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 = ∏ x ∈ s \ t ∪ t, f x

Tactic:
sdiff_union_self_eq_union,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ t ∪ s, f x = ∏ x ∈ s \ t ∪ t, f x
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, f x = ∏ x ∈ s \ t ∪ t, f x

Tactic:
sdiff_union_self_eq_union,

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s : Finset ι
a : ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
ha : a ∉ s
f : ι → G
⊢ (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
⊢ 0 * a = 0

Tactic:
have h : 0 * a + 0 * a = 0 * a := by simp [← add_mul]

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
h : 0 * a + 0 * a = 0 * a
⊢ 0 * a = 0
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)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ Subgroup.map (QuotientGroup.mk' N) (Subgroup.map H.subtype ⊤) = ⊤

Tactic:
← this,

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 := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ Subgroup.map (QuotientGroup.mk' N) (Subgroup.map H.subtype ⊤) = Subgroup.map (QuotientGroup.mk' N) ⊤
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y : FreeAbelianGroup α
s : α
⊢ of s * y = y * of s

Tactic:
induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]

Goal state after:
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 : (fun n ↦ n • of default) ((lift fun x ↦ 1) x) = x
hy : (fun n ↦ n • of default) ((lift fun x ↦ 1) y) = y
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) (x + y)) = x + y

Tactic:
simp only [map_add, add_smul] at *
      rw [hx, hy]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (map ⇑f.symm) ((map ⇑f) x) = x

Tactic:
by rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
rw [← map_zero f]
  exact OrderHomClass.mono _ ha

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ 0

Tactic:
rw [← map_zero f]
  exact OrderHomClass.mono _ ha

Goal state after: