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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H

Tactic:
simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
⊢ Monotone fun i ↦ (take i L).prod

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
⊢ (take n L).prod ≤ (take (n + 1) L).prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ ∀ (y : N) (z : α), (1 • y) • z = 1 • y • z

Tactic:
intro y z
    rw [one_smul, one_smul]

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

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (n : N) (a : α), 1 • n • a = n • 1 • a

Tactic:
intro y z
    rw [one_smul, one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl

Tactic:
simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m

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

Goal state before:
pp: case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive s

Tactic:
rw [← insert_erase H]

Goal state after:
case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)

Tactic:
induction s using Multiset.induction generalizing n with
  | empty => cases n <;> simp [powersetCard_zero_left]
  | cons t s ih => cases n <;> simp [ih]

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

Goal state before:
pp: case cons.inl
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ a :: l₂' ~ a :: l

Tactic:
exact perm_middle.trans ((IH _ _ h).cons _)

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

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = l.toFinset.sup id

Tactic:
sup_def,

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (Multiset.map id l.toFinset.val).sup
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 : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ (cons c t hc).sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
| cons c t hc ih =>

Goal state after:
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 < (cons c t hc).sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
| cons c t hc ih =>

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 : ↑(Finset.cons b t hbt) ⊆ ⋃ i, f i
⊢ ∃ i, ↑(Finset.cons b t hbt) ⊆ f i

Tactic:
simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩

Goal state after:
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)
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi

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
⊢ f ⋯ ∈ upperBounds (⋃ i_1, range fun x ↦ f ⋯)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
· exact (ciSup_neg hj).le

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
⊢ t = s ∨ t = insert x s

Tactic:
by_cases h : x ∈ t

Goal state after:
case pos
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s
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 : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ Function.update a i ci ≤ b

Tactic:
simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
refine ⟨i, fun j hj ↦ ?_⟩

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
⊢ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
⊢ a ⋖ b ↔ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
by
  simp [covBy_iff_antisymmRel]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ ⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩

Tactic:
← Finset.iSup_coe,

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ ⨆ x ∈ ↑(s.sigma t), f x = ⨆ x ∈ ↑s, ⨆ x_1 ∈ ↑(t x), f ⟨x, x_1⟩
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:
by
  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.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b

Tactic:
by rw [Ico, ← Finset.mem_def, Finset.mem_Ico]

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

Tactic:
and_assoc,

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✝¹ : 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

Tactic:
and_assoc,

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.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Iic n

Tactic:
by
  rw [range_succ_eq_Icc_zero]
  rfl

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

Goal state before:
pp: case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
have hn := Nat.mod_add_div n a

Goal state after:
case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

Tactic:
refine Or.inr <| fun m n hmn ↦ lt_of_le_of_ne ?_ ((f.injective.comp g.injective).ne ?_)
    · grind
    · grind

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
⊢ ∃ f, StrictMono f ∨ StrictAnti f

Tactic:
by
  let f := Infinite.natEmbedding α
  obtain ⟨g, hg⟩ := exists_increasing_or_nonincreasing_subseq (· < ·) f
  refine ⟨f ∘ g, ?_⟩
  rcases hg with hIncreasing | hNonincreasing
  · exact Or.inl hIncreasing
  · refine Or.inr <| fun m n hmn ↦ lt_of_le_of_ne ?_ ((f.injective.comp g.injective).ne ?_)
    · grind
    · grind

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

Goal state before:
pp: a : ℕ
⊢ (range a).toFinset = Finset.range a

Tactic:
by
  ext x
  rw [List.mem_toFinset, List.mem_range, Finset.mem_range]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ici a ⊂ Ici b ↔ b < a

Tactic:
by
  simp [← coe_ssubset]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic a ⊂ Iic b ↔ a < b

Tactic:
by
  simp [← coe_ssubset]

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

Goal state before:
pp: case mem
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x : N
hx : x ∈ s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)

Tactic:
| mem x hx =>

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
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ False

Tactic:
refine infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)

Goal state after:
case refine_1
α : 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)
m n : ℕ
hmn : f m = f n
⊢ m = n

case refine_2
α : 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)
⊢ IsAntichain r (range f)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
this : ∀ (g : M), g * ↑c = ↑c * g
⊢ c • r • v = r • c • v

Tactic:
simp_rw [Submonoid.smul_def, smul_smul, this]

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

Goal state before:
pp: case mem
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 : G
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x

Tactic:
| mem x hx =>

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

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a

Tactic:
rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd * tl.prod = hd * a * tl.prod

case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute
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:
rw [mul_smul]

Goal state after:
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
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommMonoid M
x✝ : M
s : Set M
x : M
hx : x ∈ s
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
| mem x hx =>

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
⊢ (∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ map Embedding.inr t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
prod_map

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ (∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ t, f (Embedding.inr x) = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
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 : H ⧸ H'
⊢ (map G' H' ↑e ⋯) ((map H' G' ↑e.symm ⋯) x) = x

Tactic:
rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
        (he ▸ G'.le_comap_map (e : G →* H))]
      simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
        MulEquiv.coe_monoidHom_refl, map_id_apply]

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 : ι → M
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
⊢ ∏ x ∈ s, f x = 1

Tactic:
induction s using Finset.strongInduction with | H s ih => ?_
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · simp
  have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]
  suffices h : ∏ x ∈ s \ {x, g x hx}, f x = 1 by
    rw [← prod_sdiff this, h, one_mul]
    cases eq_or_ne (g x hx) x with
    | inl hx' => simpa [hx'] using hg₃ x hx
    | inr hx' => grind
  suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} from
    ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _
      (by simp [hg₁]) (fun _ _ => hg₃ _ _) h₃ (fun _ _ => hg₄ _ _)
  grind

Goal state after:
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}
h_base : base = Group.conjugatesOfSet base
⊢ (closure base).Normal

Tactic:
by
    rw [h_base]
    exact Subgroup.normalClosure_normal

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 ≤ a → 0 ≤ f a
a b : α
hl : a ≤ b
⊢ f a ≤ f b

Tactic:
rw [← sub_add_cancel b a, map_add f]
    exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)

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
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ ↑(u * s₂) ∈ S

Tactic:
hs₂

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ ↑⟨v * ↑s₁, s₁vS⟩ ∈ S
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {x y z : M × ↥S},
    (∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)) →
      (∃ c, ↑c * (↑z.2 * y.1) = ↑c * (↑y.2 * z.1)) → ∃ c, ↑c * (↑z.2 * x.1) = ↑c * (↑x.2 * z.1)

Tactic:
rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
    use t₂ * t₁ * b.2
    simp only [Submonoid.coe_mul]
    calc
      (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
      _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl

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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ ↑s₃ * (↑u₀ * r₁) = ↑s₃ * (v₀ * ↑s₂)

Tactic:
h₀

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ ↑s₃ * (v₀ * ↑s₂) = ↑s₃ * (v₀ * ↑s₂)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
by
  rw [map, lift_mk', mul_inv_left]
  change k (g x) = k (g y) * _
  rw [mul_mk'_eq_mk'_of_mul]
  exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
x : N
⊢ (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x

Tactic:
rw [← f.map_comp_map (k := k) hy j hl]
  simp only [MonoidHom.coe_comp, comp_apply]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
z : Localization S
x : M × ↥S
⊢ mk (↑x.2) x.2 * mk x.1 1 = mk x.1 1

Tactic:
mk_self,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
z : Localization S
x : M × ↥S
⊢ 1 * mk x.1 1 = mk x.1 1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : Bijective ⇑f
e : G ≃* M := { toEquiv := Equiv.ofBijective (⇑f) h, map_mul' := ⋯ }
x✝ y✝ : G
eq : f x✝ = f y✝
⊢ ∃ c, ↑c * x✝ = ↑c * y✝

Tactic:
by simp [h.1 eq]

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

Tactic:
bot_mul hb,

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