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

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
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
g : N →* G
h : LeftInverse ⇑g ⇑f
⊢ RightInverse (⇑g ∘ ⇑f.range.subtype) ⇑f.rangeRestrict

Tactic:
rintro ⟨x, y, rfl⟩

Goal state after:
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
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
g : N →* G
h : LeftInverse ⇑g ⇑f
y : G
⊢ f.rangeRestrict ((⇑g ∘ ⇑f.range.subtype) ⟨f y, ⋯⟩) = ⟨f y, ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.Ker

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
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ Surjective ⇑(f.codRestrict f.range ⋯)

Tactic:
rintro ⟨x, y, rfl⟩

Goal state after:
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
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
hf : Injective ⇑f
y : G
⊢ ∃ a, (f.codRestrict f.range ⋯) a = ⟨f y, ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ map f H = map f ⊤ ↔ Codisjoint H f.ker

Tactic:
map_eq_map_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ H ⊔ f.ker = ⊤ ⊔ f.ker ↔ Codisjoint H f.ker
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
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
I : Set ι
x : (i : ι) → M i
⊢ (x ∈ pi I fun i ↦ ⊤) ↔ x ∈ ⊤

Tactic:
simp [mem_pi]

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
H : (i : ι) → Submonoid (M i)
x : (i : ι) → M i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤

Tactic:
simp [mem_pi]

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
x : (i : η) → f i
⊢ (x ∈ pi I fun i ↦ ⊤) ↔ x ∈ ⊤

Tactic:
simp [mem_pi]

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
x : (i : η) → f i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤

Tactic:
simp [mem_pi]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ zpowers g ≤ H ↔ g ∈ H

Tactic:
by
  rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
rw [normal_le_normalCore]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H
Module: Mathlib.Algebra.FreeMonoid.Basic

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

Tactic:
by
  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.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ (hd :: tl).prod

Tactic:
rw [prod_cons]
    exact one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)

Tactic:
rw [disjoint_map_map]

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → inl a ≠ inr b
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = l.maximum

Tactic:
induction l with
  | nil => contradiction
  | cons hd tl IH =>
    rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]

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

Goal state before:
pp: case nil
α : Type u
⊢ flatMap (fun n ↦ sublistsLen n []) (range ([].length + 1)) ~ [].sublists'

Tactic:
simp [range_succ]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄,
    i ∈ ↑s.powerset → ∀ ⦃j : Finset α⦄, j ∈ ↑s.powerset → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
mem_coe,

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄,
    i ∈ s.powerset → ∀ ⦃j : Finset α⦄, j ∈ s.powerset → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr.refine_2
α : 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
⊢ f (j, j') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (j, j').1

Tactic:
· convert! le_iSup₂ (α := α) j' hj.2; rfl

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∈ s
⊢ ∃ a ∈ s, f i ≤ f a

Tactic:
exact ⟨_, by assumption, le_rfl⟩

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

Goal state before:
pp: case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t

Tactic:
rintro ⟨i, -, H⟩
      exact H

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

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
by_cases! hg : ¬BddAbove (range g)

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
by
  have := hne.to_subtype
  rw [image_eq_range] at hf
  exact gc.l_ciSup hf

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
⊢ a ⋖ b → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⋖ b

Tactic:
· intro h
    obtain ⟨j, hj⟩ := (Pi.lt_def.1 h.1).2
    have : Nonempty ι := ⟨j⟩
    obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h.wcovBy
    obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj
    exact ⟨i, covBy_iff_wcovBy_and_lt.2 ⟨h.wcovBy.eval i, hj⟩, hi⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⋖ b
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
e : α ≃ β
s : Finset β
⊢ Finset.image (⇑e.symm) s = s.preimage ⇑e ⋯

Tactic:
by
  grind [Finset.mem_preimage]

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

Goal state before:
pp: case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s

Tactic:
intro H
    rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
    · exact ⟨le_rfl, k.not_succ_le_self⟩
    · exact k
    · assumption

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ r (f (n + m)) (f (n + n' - n - m + m))

Tactic:
convert! hn2

Goal state after:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ n + n' - n - m + m = n'
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : BoundedOrder α
inst✝ : Fintype α
⊢ Icc ⊥ ⊤ = univ

Tactic:
by
  rw [Icc_bot, Iic_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLT α
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ Finset.subtype (fun x ↦ x < y) (Ico (↑a) y) ↔ a ≤ b

Tactic:
simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]
    exact fun _ => b.property

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
⊢ g ∈ center G

Tactic:
mem_center_iff

Goal state after:
G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
⊢ ∀ (g_1 : G), g_1 * g = g * g_1
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∈ center G
b : G
⊢ b * a * b⁻¹ ∈ center G

Tactic:
simpa [mem_center_iff.mp ha b]

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

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
hx : x ∈ Set.center M
⊢ e x ∈ Set.center N

Tactic:
by
  let e := MulEquivClass.toMulEquiv e
  change e x ∈ Set.center N
  constructor <;>
  (intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm])

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ normalizer ↑H ⊓ normalizer ↑K ≤ normalizer ↑(H ⊔ K)

Tactic:
by
  intro g hg
  simp_rw [mem_inf, mem_normalizer_iff_map_conj_eq, map_sup, hg.1, hg.2] at hg ⊢

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
⊢ (fun i ↦ Quotient.mk'' (x i)) = fun i ↦ Quotient.mk'' (y i)

Tactic:
ext i
    simpa [Quotient.eq] using hxy i

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

Goal state before:
pp: case trans.inr
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ z✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ x✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ z✝
ih2 : (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ z✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ z✝

Tactic:
exact ih2

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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by
  have := Classical.decEq ι; by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s
  · exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀
  · rw [hb h₂, mul_one]
    apply prod_eq_single_of_mem a h₁
    exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩
  · rw [ha h₁, one_mul]
    apply prod_eq_single_of_mem b h₂
    exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩
  · rw [ha h₁, hb h₂, mul_one]
    exact
      _root_.trans
        (prod_congr rfl fun c hc =>
          h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
        prod_const_one

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : Monoid M
S : Set M
hfin : Finite ↑S
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
⊢ FG M

Tactic:
refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩

Goal state after:
case refine_2
M : Type u_1
inst✝ : Monoid M
S : Set M
hfin : Finite ↑S
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
⊢ Submonoid.closure (⇑φ '' Set.range FreeMonoid.of) = ⊤
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
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ x ∈ ((mk' M).comp f).ker

Tactic:
refine QuotientGroup.eq.2 ?_

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
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ (f x)⁻¹ * 1 ∈ M
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ (toAddSubgroup P).FG

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

Goal state after:
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ (toAddSubgroup P).FG
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 => ?_

Goal state after:
case H
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
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
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

Tactic:
prod_range_div,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = f 0 * (f n / f 0)
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 : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ s • (t • r, ⟨t * ↑s, hst⟩).fst = (↑s * t) • (r, s).fst

Tactic:
by rw [mul_smul, Submonoid.smul_def]

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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
y : ↥S
⊢ f ((f.sec (f.mk' x y)).1 * ↑y) = f (x * ↑(f.sec (f.mk' x y)).2)

Tactic:
simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]

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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ (f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1

Tactic:
lift_mul_right

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g (f.sec z).1 = g (f.sec z).1
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
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z

Tactic:
rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑1 = f ↑y * z
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
s t : ↥S
⊢ r₁ * ↑s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t

Tactic:
simp [oreDiv_mul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
by
      have : ∀ z, map f z = 0 ↔ z = 0 := fun z =>
        (Option.map_injective hf).eq_iff' f.toZeroHom.withTopMap.map_zero
      rcases Decidable.eq_or_ne x 0 with (rfl | hx)
      · simp
      rcases Decidable.eq_or_ne y 0 with (rfl | hy)
      · simp
      cases x with | top => simp [hy, this] | coe x => ?_
      cases y with
      | top =>
        have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
        simp [mul_top hx, mul_top this]
      | coe y => simp [← coe_mul]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LT α
⊢ IsSuccPrelimit (toDual a) ↔ IsPredPrelimit a

Tactic:
simp [IsSuccPrelimit, IsPredPrelimit]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : a✝ < a✝¹
⊢ (if succ a✝ = a✝ then ⊤ else ↑(succ a✝)) ≤ ↑a✝¹

Tactic:
split_ifs with ha

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : a✝ < a✝¹
ha : succ a✝ = a✝
⊢ ⊤ ≤ ↑a✝¹

case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : a✝ < a✝¹
ha : ¬succ a✝ = a✝
⊢ ↑(succ a✝) ≤ ↑a✝¹
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b : WithBot ℕ∞
c : ℕ
⊢ a + ↑c ≤ b + ↑c ↔ a ≤ b

Tactic:
WithBot.add_le_add_natCast_right_iff

Goal state after:
a b : WithBot ℕ∞
c : ℕ
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
_hx : x ∈ univ
⊢ p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
_hx : x ∈ univ
⊢ ¬p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s✝ : Finset ι
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

Goal state after: