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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
| ∀ (i : β), ⨆ c, f (i, c) ≤ c

Tactic:
enter [b]; rw [ciSup_le_iff (h₂ b)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ∀ (i : γ), f (b, i) ≤ c
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
⊢ BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)

Tactic:
by
  induction I, H using Set.Finite.induction_on with
  | empty => simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]
  | insert _ _ hs => simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x = c
hac : a ≤ c
hcb : c < b
⊢ a = c ∧ a ⋖ b

Tactic:
obtain rfl := (h a).mp ⟨le_refl a, hac.trans_lt hcb⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x = a
hac : a ≤ a
hcb : a < b
⊢ a = a ∧ a ⋖ b
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(sigmaLift f a b) = if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0

Tactic:
simp_rw [sigmaLift]
  split_ifs with h <;> simp

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ Minimal (fun x ↦ P ↑x) ⟨x, hx⟩ ↔ Minimal (P ⊓ Q) ↑⟨x, hx⟩

Tactic:
simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]

Goal state after:
α : Type u_2
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ (P x ∧ ∀ (a : α), Q a → P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ⇑f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x}

Tactic:
by
  convert! _root_.image_monotone_setOfPred_minimal (f := f) (by simp [f.le_iff_le])
  aesop

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x

Tactic:
by rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ (orderIsoOfNat s) n = ofNat s n

Tactic:
simp only [orderIsoOfNat, RelIso.ofSurjective_apply,
    RelEmbedding.orderEmbeddingOfLTEmbedding_apply, RelEmbedding.coe_natLT]
  congr!

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

Goal state before:
pp: case inl
n : ℕ
⊢ image (fun x ↦ x % 0) ∅ = ∅

Tactic:
image_empty

Goal state after:
case inl
n : ℕ
⊢ ∅ = ∅
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case zero
⊢ image (fun j ↦ 0 - 1 - j) ∅ = ∅

Tactic:
image_empty

Goal state after:
case zero
⊢ ∅ = ∅
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
refine ⟨⟨f, ?_⟩⟩

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]

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

Goal state before:
pp: case e'_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ MulAction.orbit ↥H ↑b = MulAction.orbit ↥H ↑a

Tactic:
orbit_eq_iff

Goal state after:
case e'_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ (n + 1) * ↑(closure s) = ↑(closure s)

Tactic:
by rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x✝¹ : G
hx✝ : x✝¹ ∈ (closure S).toSubmonoid
x : G
x✝ : x ∈ closure S
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)⁻¹

Tactic:
Set.union_inv,

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x✝¹ : G
hx✝ : x✝¹ ∈ (closure S).toSubmonoid
x : G
x✝ : x ∈ closure S
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x ∈ Submonoid.closure (S⁻¹ ∪ S⁻¹⁻¹)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul_left.inr
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x✝ : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : y ∈ Submonoid.closure (s ∪ s⁻¹)
ih : p y ⋯
hx : x ∈ s⁻¹
⊢ p (x * y) ⋯

Tactic:
simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

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

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, hmul _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T

Tactic:
simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
h : ∀ (i : ConjAct G), i⁻¹ • g ∈ H
x : G
⊢ x * g * x⁻¹ ∈ H

Tactic:
simpa only [ConjAct.toConjAct_inv, inv_inv] using! h x⁻¹

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

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

Tactic:
obtain ⟨f, t, hts, hf, rfl⟩ := hx

Goal state after:
case mul
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
y : M
hy✝ : y ∈ closure s
hy : ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = y
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
⊢ ∃ f_1 t_1, ↑t_1 ⊆ s ∧ Function.support f_1 ⊆ ↑t_1 ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * y
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
⊢ ¬Step [] L

Tactic:
generalize h' : [] = L'
  intro h
  rcases h with - | ⟨L₁, L₂⟩
  simp at h'

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f g : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i

Tactic:
rw [← prod_sdiff h, prod_eq_one hg, one_mul]
  exact prod_congr rfl hfg

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
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
j : κ
x✝ : j ∈ t
i : ι
hi : i ∈ {i ∈ s | g i = j}
⊢ f j = f (g i)

Tactic:
by rw [(mem_filter.1 hi).2]

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

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)

Tactic:
induction L1 with
    | nil =>
      rw [nil_append, nil_append, cons.sizeOf_spec, cons.sizeOf_spec]
      lia
    | cons hd tl ih =>
      dsimp
      exact Nat.add_lt_add_left ih _

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : g (FreeGroup.mk t) = (map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ g (FreeGroup.of x * FreeGroup.mk t) = (map f) (FreeGroup.of x * FreeGroup.mk t)

Tactic:
simp [g.map_mul, hg, ih]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N

Tactic:
nN.mem_comm_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x * y⁻¹ ∈ N ↔ x / y ∈ N
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
this : Fintype ι
⊢ (Submonoid.pi Set.univ P).FG

Tactic:
choose s hs using hP

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ (Submonoid.pi Set.univ P).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: 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

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Goal state after:
case H.inl
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
ih :
  ∀ t ⊂ ∅,
    ∀ (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 ∈ ∅ → ι
hg₁ : ∀ (a : ι) (ha : a ∈ ∅), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ ∅), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ ∅), g a ha ∈ ∅
hg₄ : ∀ (a : ι) (ha : a ∈ ∅), g (g a ha) ⋯ = a
⊢ ∏ x ∈ ∅, f x = 1

case H.inr
ι : 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 : ι
hx : x ∈ s
⊢ ∏ x ∈ s, f x = 1
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' mk '' s → a ∈ ↑N * s

pp: case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ ↑N * s → a ∈ mk ⁻¹' mk '' s

Tactic:
· rintro ⟨b, hb, h⟩
    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
    simp only [h, QuotientGroup.mk_div, div_self']

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ ↑N * s → a ∈ mk ⁻¹' mk '' s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
by
  refine prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j hdisj hfij ↦ ?_
  rw [Function.onFun, ← hfij, disjoint_self] at hdisj
  rw [hdisj, hg_bot]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
try rw [ihx, ihy]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
try rw [ihx, ihy]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ∀ h ∈ H₁,
    ∀ g ∈ {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}, h * g * h⁻¹ ∈ closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}

Tactic:
rintro g hg _ ⟨g₁, hg₁, g₂, hg₂, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ g * ⁅g₁, g₂⁆ * g⁻¹ ∈ closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
apply le_antisymm
  · rw [commutator_le]
    rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
    exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
  · rw [prod_le_iff]
    constructor <;>
      · rw [map_commutator]
        apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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 y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ g x = g y

Tactic:
← one_mul (g x),

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)
x y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ 1 * g x = g y
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f g : α →*o β
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (a : α), f a = g a

Tactic:
by convert! DFunLike.ext_iff.1 h using 0

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f g : α →*o β
h : f.toOrderHom = g.toOrderHom
⊢ ∀ (a : α), f a = g a

Tactic:
by convert! DFunLike.ext_iff.1 h using 0

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f g : α ≃*o β
h : f.toMulEquiv = g.toMulEquiv
⊢ ∀ (a : α), f a = g a

Tactic:
by convert! DFunLike.ext_iff.1 h using 0

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f g : α ≃*o β
h : f.toOrderIso = g.toOrderIso
⊢ ∀ (a : α), f a = g a

Tactic:
by convert! DFunLike.ext_iff.1 h using 0

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

Goal state before:
pp: case e'_2.e'_3
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ f (f.symm a) = a

Tactic:
exact f.toEquiv.apply_symm_apply _

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

Goal state before:
pp: case e'_2.e'_4
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ f (f.symm b) = b

Tactic:
exact f.toEquiv.apply_symm_apply _

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

Goal state before:
pp: case h.left
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
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * (↑s₃ * v₀)) • r₂ = (↑s₄ * r₃) • v • r₂

Tactic:
← hs₄

Goal state after:
case h.left
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
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * (r₃ * v)) • r₂ = (↑s₄ * r₃) • v • r₂
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulZeroOneClass α
inst✝ : MulZeroOneClass β
f g : α →*₀o β
h : f.toOrderMonoidHom = g.toOrderMonoidHom
⊢ ∀ (a : α), f a = g a

Tactic:
by convert! DFunLike.ext_iff.1 h using 0

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulZeroOneClass α
inst✝ : MulZeroOneClass β
f g : α →*₀o β
h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (a : α), f a = g a

Tactic:
by convert! DFunLike.ext_iff.1 h using 0

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
y : OreLocalization S R
x : OreLocalization S X
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
⊢ smul'' r₁ s x = smul'' (r₂ • r₁) ⟨r₂ * ↑s, hs⟩ x

Tactic:
cases x with | _ x s₂
    change OreLocalization.smul' r₁ s x s₂ = OreLocalization.smul' (r₂ * r₁) ⟨_, hs⟩ x s₂
    rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩
    rw [smul'_char _ _ _ _ _ _ h₁]
    rcases oreCondition (r₂ * r₁) s₂ with ⟨r₂', s₂', h₂⟩
    rw [smul'_char _ _ _ _ _ _ h₂]
    rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩
    have : s₃' * r₂' * s₂ = r₃' * r₁' * s₂ := by
      rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]
    rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩
    have : (s₄' * r₃') * (s₁' * s) ∈ S := by
      rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
      exact mul_mem (s₄' * s₃' * s₂').2 hs
    rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ this]
    simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]
    congr 1
    ext; simp only [Submonoid.coe_mul, ← mul_assoc]
    rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc]

Goal state after:
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 : S.LocalizationMap N
x y : M
c : ↥S
h : f (x * ↑c) = f (y * ↑c)
⊢ f (x * ↑c) = f (↑c * y)

Tactic:
mul_comm _ y,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f (x * ↑c) = f (y * ↑c)
⊢ f (x * ↑c) = f (y * ↑c)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case inl
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
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : c * z' = c * w'
⊢ f z' = w * f ↑x

Tactic:
hxw,

Goal state after:
case inl
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
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : c * z' = c * w'
⊢ f z' = f w'