mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Setoid.Basic

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

Tactic:
rcases ih1 with ih1 | rfl

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

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✝
Module: Mathlib.Data.Setoid.Basic

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

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:
· rcases ih2 with ih2 | rfl
      · exact .inl <| r.iseqv.isTrans.map hf |>.trans _ _ _ ih1 ih2
      · exact .inl ih1

Goal state after:
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✝
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : r x y
⊢ (comap Quotient.mk' s) x y

Tactic:
comap_rel,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : r x y
⊢ s (Quotient.mk' x) (Quotient.mk' y)
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
h :
  { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      s ≤
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      t
x y : M
hs : ↑s x y
⊢ ↑t x y

Tactic:
rcases h ⟨x, y, hs, rfl, rfl⟩ with ⟨a, b, ht, hx, hy⟩

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
h :
  { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      s ≤
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      t
x y : M
hs : ↑s x y
a b : M
ht : (↑t).toSetoid a b
hx : c.mkMulHom a = c.mkMulHom x
hy : c.mkMulHom b = c.mkMulHom y
⊢ ↑t x y
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
P : AddSubmonoid M
⊢ P.FG ↔ (toSubmonoid P).FG

Tactic:
by
  convert! (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

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

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
c : Con G
x : G
hx : x ∈ c.subgroup
g : G
⊢ g * x * g⁻¹ ∈ c.subgroup

Tactic:
simpa using (c.mul (c.mul (c.refl g) hx) (c.refl g⁻¹))

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
⊢ QuotientGroup.con c.subgroup = c

Tactic:
ext x y
  rw [QuotientGroup.con, Con.rel_mk, leftRel_apply, Con.mem_subgroup_iff]
  exact ⟨fun h ↦ by simpa using c.mul (c.refl x) (c.symm h),
    fun h ↦ by simpa using c.mul (c.refl x⁻¹) (c.symm h)⟩

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

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
x✝ : x ∈ s
hx : x ∉ m.toFinset
⊢ x ^ count x m = 1

Tactic:
mem_toFinset

Goal state after:
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
x✝ : x ∈ s
hx : x ∉ m
⊢ x ^ count x m = 1
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
← hS,

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

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

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

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG

Tactic:
exact .pi hP

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 : α✝
⊢ pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g

Tactic:
pure_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
⊢ f x >>= g = pure x >>= 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 : α✝
⊢ f x >>= g = pure x >>= fun x ↦ f x >>= g

Tactic:
pure_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
⊢ f x >>= g = f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
apply prod_range_induction <;> simp

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

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

Tactic:
apply prod_range_induction <;> simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
f : ι → M
s : Finset ι
t : Finset M
H : Set.MapsTo f ↑s ↑t
⊢ #s = ∑ b ∈ t, #({a ∈ s | f a = b})

Tactic:
by
  simp only [card_eq_sum_ones, sum_fiberwise_of_maps_to H]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x = x

Tactic:
induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, mul_one]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) x * (QuotientGroup.mk' N) y = (QuotientGroup.mk' N) y * (QuotientGroup.mk' N) x

Tactic:
← commutatorElement_eq_one_iff_mul_comm,

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅(QuotientGroup.mk' N) x, (QuotientGroup.mk' N) y⁆ = 1
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)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ g (f.sec x✝).1 = g ↑(f.sec x✝).2 * j x✝

Tactic:
← hj,

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)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ j (f (f.sec x✝).1) = g ↑(f.sec x✝).2 * j x✝
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)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ j (f (f.sec x✝).1) = g ↑(f.sec x✝).2 * j x✝

Tactic:
← hj,

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)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ j (f (f.sec x✝).1) = j (f ↑(f.sec x✝).2) * j x✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
h₂

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
⊢ r₃' * (r₂' * ↑⟨r₂ * ↑s', hs⟩) = r₃' * r₂' * r₂ * ↑s'
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
rw [mul_assoc (s₄' : R), h₃, ← 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 : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑y = f ↑z

Tactic:
← mul_one (f y),

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑y * 1 = f ↑z
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₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

Tactic:
refine (mul_inv_left f.map_units _ _ _).2 ?_

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₁ x₂ : M
y₁ y₂ : ↥S
⊢ f (x₁ * x₂) = f.toMonoidHom ↑(y₁ * y₂) * (f.mk' x₁ y₁ * f.mk' x₂ y₂)
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₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * f x₂ = f ↑y₁ * f ↑y₂ * (f x₁ * ↑⋯.unit⁻¹ * (f x₂ * ↑⋯.unit⁻¹))

Tactic:
rw [mul_mul_mul_comm (f x₁), mul_left_comm, mul_mul_mul_comm (f 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₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * f x₂ = f x₁ * f x₂ * (f ↑y₁ * ↑⋯.unit⁻¹ * (f ↑y₂ * ↑⋯.unit⁻¹))
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
⊢ 1 = 1 /ₒ 1

Tactic:
OreLocalization.one_def

Goal state after:
case zero
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
⊢ 1 /ₒ 1 = 1 /ₒ 1
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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
⊢ ↑(fS s)⁻¹ * f r = ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * ↑(fS ⟨t * ↑s, ht⟩) * (↑(fS s)⁻¹ * f r)

Tactic:
simp only [one_mul, Units.inv_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S'✝ : Type u_6
inst✝⁶ : NonUnitalNonAssocSemiring R✝
inst✝⁵ : NonUnitalNonAssocSemiring S✝
f✝ : R✝ ≃+* S✝
x : R✝
inst✝⁴ : FunLike F R✝ S✝
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring R'
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
x✝¹ x✝ : R × S
⊢ ((↑f).prodCongr ↑g).toFun (x✝¹ + x✝) = ((↑f).prodCongr ↑g).toFun x✝¹ + ((↑f).prodCongr ↑g).toFun x✝

Tactic:
simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, map_add, Prod.mk_add_mk]

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

Goal state before:
pp: case h
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 : S.IsLocalizationMap ⇑f
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ m * f 1 = m

Tactic:
h.map_one,

Goal state after:
case h
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 : S.IsLocalizationMap ⇑f
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ m * 1 = m
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Tactic:
· exact fun k hk => hy _ (hk.trans n.lt_succ_self)

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

Goal state before:
pp: case inr
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb✝ : b ∈ s
hb : b < a
⊢ ¬IsMin a

Tactic:
· exact hb.not_isMin

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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ cast ⋯ (succ (Classical.choose ⋯) ⋯) = succ b hb

Tactic:
cast_eq_iff_heq

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ succ (Classical.choose ⋯) ⋯ ≍ succ b hb
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x - 1 < y
⊢ x ≤ y

Tactic:
by
  rw [← pred_eq_sub_one] at h
  exact le_of_pred_lt h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
y : Y
⊢ y ≤ f (succ (f.symm y))

Tactic:
rw [← map_inv_le_iff f]; exact le_succ (f.symm y)

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

Goal state before:
pp: case coe
n a✝ : ℕ
⊢ (↑a✝ - ↑n).toNat = (↑a✝).toNat - (↑n).toNat

Tactic:
· rw [← natCast_sub, toNat_natCast, toNat_natCast, toNat_natCast]

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise f (update g i v)

Tactic:
by
  rw [update_piecewise]
  refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl
  exact fun h => hi (h ▸ hj)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Tactic:
simp only [piecewise]

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head ∈ v.head :: v.tail.toList

Tactic:
List.mem_cons

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head = v.head ∨ v.head ∈ v.tail.toList
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.head :: v.tail.toList

Tactic:
List.mem_cons

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x = v.head ∨ x ∈ v.tail.toList
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List α
⊢ map (⇑e.symm) (map (⇑e) l) = l

Tactic:
List.map_map,

Goal state after:
α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List α
⊢ map (⇑e.symm ∘ ⇑e) l = l
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ map (⇑e) (map (⇑e.symm) l) = l

Tactic:
List.map_map,

Goal state after:
α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ map (⇑e ∘ ⇑e.symm) l = l
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n ⊕ Sym α n.succ
⊢ encode (decode s) = s

Tactic:
obtain s | s := s

Goal state after:
case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s

case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x

pp: case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x

Tactic:
· obtain (rfl | h) := (trichotomous y x).resolve_left hs
    · exact hy
    · obtain ⟨z, rfl⟩ := hy
      exact f.mem_range_of_rel h

Goal state after:
case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB ((fun x ↦ (f x, g x)) '' d) ((fun x ↦ (f x, g x)) a)

Tactic:
by
  rw [IsLUB, IsLeast, upperBounds]
  constructor
  · simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq,
      Prod.mk_le_mk]
    intro b hb
    exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩
  · intro ⟨p₁, p₂⟩ hp
    simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq,
      Prod.mk_le_mk] at hp
    constructor
    · rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq]
      intro _ hb
      exact (hp _ hb).1
    · rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq]
      intro _ hb
      exact (hp _ hb).2

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
⊢ ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False

Tactic:
h₂

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
⊢ False