mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
· exact Step.cons_not

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, g.map_inv, hg, ih]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
closure_range_of

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0

Tactic:
prod_range_succ _ n,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f (n + 1) * f 0
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
h : c x y
⊢ c (x⁻¹ * y) 1

Tactic:
simpa using c.mul (c.refl x⁻¹) (c.symm h)

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

Tactic:
· rintro ⟨S, hS⟩
    refine ⟨S, le_antisymm ?_ ?_⟩
    · rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
      exact Submonoid.subset_closure
    · rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
      exact Subgroup.subset_closure

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
exact (Subgroup.toSubmonoid P).fg_iff_add_fg

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.LeftInverse ⇑(Abelianization.map e.symm.toMonoidHom) ⇑(Abelianization.map e.toMonoidHom)

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization G
a : G
⊢ (Abelianization.map e.symm.toMonoidHom)
      ((Abelianization.map e.toMonoidHom) (Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a)) =
    Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a
Module: Mathlib.GroupTheory.Abelianization.Defs

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.RightInverse ⇑(Abelianization.map e.symm.toMonoidHom) ⇑(Abelianization.map e.toMonoidHom)

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization H
a : H
⊢ (Abelianization.map e.toMonoidHom)
      ((Abelianization.map e.symm.toMonoidHom) (Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a)) =
    Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a
Module: Mathlib.GroupTheory.Abelianization.Defs

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
⊢ Function.RightInverse ⇑(lift (MonoidHom.id H)) ⇑of

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
x✝ : Abelianization H
a : H
⊢ of ((lift (MonoidHom.id H)) (Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a)) =
    Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a
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
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y = 1

Tactic:
← Finset.prod_eq_one

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y = ∏ x ∈ ?m.38, ?m.40 x

ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∀ x ∈ ?m.38, ?m.40 x = 1

ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ Type ?u.54

ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ Finset ?m.36

ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ?m.36 → M
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ (↑s).PairwiseDisjoint t'

Tactic:
intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

Tactic:
commutatorElement_def,

Goal state after:
G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ g₁ * g₂ * g₁⁻¹ * g₂⁻¹ = 1 ↔ g₁ * g₂ = g₂ * g₁
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
commutatorElement_def,

Goal state after:
G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ (g₁ * g₂ * g₁⁻¹ * g₂⁻¹)⁻¹ = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
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
⊢ f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

Tactic:
commutatorElement_def,

Goal state after:
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
⊢ f (g₁ * g₂ * g₁⁻¹ * g₂⁻¹) = f g₁ * f g₂ * (f g₁)⁻¹ * (f g₂)⁻¹
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ = ⊥ ↔ H ≤ center G

Tactic:
rw [commutator_comm, commutator_top_right_eq_bot_iff_le_center]

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

Goal state before:
pp: 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⁻¹ * ⁅g, g₂⁆ ∈ ⁅H₁, H₂⁆

Tactic:
← commutatorElement_mul_left_eq_conj_mul g g₁ g₂

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₂⁆ ∈ ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
⊢ ∀ g₂ ∈ H₂, ⁅f p, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
q

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
⊢ q ∈ H₂ → ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆

Tactic:
_root_.commutator_def,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype ⁅⊤, ⊤⁆ = ⁅H, H⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g

Tactic:
commutatorElement_def,

Goal state after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ↑h * g * (↑h)⁻¹ * g⁻¹ = g
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f (commutator G) = ⁅f.range, f.range⁆

Tactic:
_root_.commutator_def,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⁅⊤, ⊤⁆ = ⁅f.range, f.range⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

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

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 × ↥S
⊢ (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

Tactic:
lift_mk',

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 × ↥S
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ = (f.lift hg) (f.mk' y.1 y.2) ↔
    g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
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 × ↥S
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ = (f.lift hg) (f.mk' y.1 y.2) ↔
    g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

Tactic:
lift_mk',

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 × ↥S
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ = g y.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) y.2)⁻¹ ↔
    g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ (f.lift hg) (f.mk' x.1 x.2) * g ↑x.2 = g x.1

Tactic:
lift_mk',

Goal state after:
case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ * g ↑x.2 = g x.1
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case h
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)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ (f.lift hg) (f.mk' x.1 x.2) = v

Tactic:
lift_mk',

Goal state after:
case h
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)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ = v
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.lift ⋯) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
lift_mk',

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k.toMonoidHom.comp g) x * ↑((IsUnit.liftRight ((k.toMonoidHom.comp g).domRestrict S) ⋯) y)⁻¹ = k.mk' (g x) ⟨g ↑y, ⋯⟩
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₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
ha'

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₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)

Tactic:
ha'

Goal state after:
case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a

Tactic:
obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le

Goal state after:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedGT α
inst✝ : SuccOrder α
⊢ IsPredArchimedean αᵒᵈ

Tactic:
by infer_instance

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

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
h : IsMin a
nh : pred ↑a ∈ s
⊢ False

Tactic:
by
    replace h := congr($h.pred_eq.1)
    rw [coe_pred_of_mem nh] at h
    simp at h

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

Goal state before:
pp: case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
· ext; simp

Goal state after:
case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
f : Fin 0 → α
⊢ nil.toList = []

Tactic:
toList,

Goal state after:
α : Type u_1
f : Fin 0 → α
⊢ ↑nil = []
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 → β
a : α
v : Vector α n
ha : p a
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x

Tactic:
simpa [ha]

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

Goal state before:
pp: α : Type u_1
v : Vector α 1
⊢ v.toList = [v.head]

Tactic:
rw [← v.cons_head_tail]
  simp only [toList_cons, toList_nil, head_cons, singleton_tail]

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

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s

Tactic:
ext; simp only [map, id_eq, Multiset.map_id', ← val_eq_coe]

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

Goal state before:
pp: case succ.cons.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : (a :: v).length = n + 1
b : β
w : List β
w_property : (b :: w).length = n + 1
⊢ C ⟨a :: v, v_property⟩ ⟨b :: w, w_property⟩

Tactic:
apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩

Goal state after:
case succ.cons.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : (a :: v).length = n + 1
b : β
w : List β
w_property : (b :: w).length = n + 1
⊢ C ⟨v, ⋯⟩ ⟨w, ⋯⟩
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
by
  obtain ⟨f, hf⟩ := Infinite.natEmbedding s hs
  refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩
  · exact fun _ ⟨y, hy⟩ ↦ hy ▸ Subtype.coe_prop (f y)
  · exact countable_range (Subtype.val ∘ f)
  · exact infinite_range_of_injective <| Injective.comp Subtype.val_injective hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)

Tactic:
induction v₁, v₂ using inductionOn₂ with

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s

Tactic:
rw [Set.preimage_iterate_eq]
  exact h.iterate n

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a ↔ ∃ c ≤ a, f c = b

Tactic:
by
  constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_le h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.le_iff_le] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.monotone hc

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous (g ∘ f)

Tactic:
rw [← scottContinuousOn_univ] at ⊢ hf hg
  exact ScottContinuousOn.comp (by simp) (by simp [MapsTo]) hg hf

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
⊢ (↑Option.none).Dom ↔ Option.none.isSome = true

Tactic:
by simp [ofOption, none]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part α✝
y : Part β✝
⊢ (x <* y).Dom ↔ (const β✝ <$> x <*> y).Dom

Tactic:
simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, (· <$> ·), and_comm]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o

Tactic:
rw [show f = id from funext H]

Goal state after:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ {y | IsExtremePt x f y}

Tactic:
refine ⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩
      intro y hy hyx
      exfalso
      exact lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
⊢ ∀ {z : α}, z ∈ bot x f → z < cSup c → f z ≤ cSup c

Tactic:
intro y hy hy'

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
⊢ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.h₂
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ (c.map { toFun := g, monotone' := ⋯ }).toOrderHom j ≤ g (c.toOrderHom (max i j))

Tactic:
apply hg.monotone (c.monotone le_sup_right)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b c : Cardinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
mul_comm b c

Goal state after:
a b c : Cardinal.{u_1}
⊢ a ^ (c * b) = (a ^ b) ^ c
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: ι : Type u
β : ι → Type v
I : Nonempty ι
⊢ ∃ s, Maximal (fun x ↦ x ∈ sets β) s

Tactic:
refine zorn_subset _ fun c hc hcc ↦
      ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩

Goal state after:
ι : Type u
β : ι → Type v
I : Nonempty ι
c : Set (Set ((i : ι) → β i))
hc : c ⊆ sets β
hcc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
i : ι
x : (i : ι) → β i
x✝¹ : x ∈ ⋃₀ c
y : (i : ι) → β i
x✝ : y ∈ ⋃₀ c
hi : (fun x ↦ x i) x = (fun x ↦ x i) y
p : Set ((i : ι) → β i)
hpc : p ∈ c
hxp : x ∈ p
q : Set ((i : ι) → β i)
hqc : q ∈ c
hyq : y ∈ q
⊢ x = y