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

Goal state before:
pp: case c
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
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ (↑s₄' * (r₃' * r₁')) • x /ₒ ⟨↑s₄' * (r₃' * (↑s₁' * ↑s)), ⋯⟩ =
    (↑s₄' * (r₃' * r₁')) • x /ₒ (s₄' * (s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩)))

Tactic:
congr 1

Goal state after:
case e_s
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
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ⟨↑s₄' * (r₃' * (↑s₁' * ↑s)), ⋯⟩ = s₄' * (s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩))
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₁ * x₂) = f.toMonoidHom ↑(y₁ * y₂) * (f.mk' x₁ y₁ * f.mk' x₂ y₂)

Tactic:
simp only [map_mul, coe_mul, toMonoidHom_apply, mk', IsUnit.liftRight, Units.liftRight,
    MonoidHom.domRestrict_apply, MonoidHom.coe_mk, OneHom.coe_mk]

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 ↑y₁ * f ↑y₂ * (f x₁ * ↑⋯.unit⁻¹ * (f x₂ * ↑⋯.unit⁻¹))
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n
⊢ Quot.mk (⇑(OreLocalization.oreEqv S M)) a = Quot.mk (⇑(OreLocalization.oreEqv S M)) b

Tactic:
change mk a.1 a.2 = mk b.1 b.2

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n
⊢ mk a.1 a.2 = mk b.1 b.2
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₂
⊢ f ra * f r₂ = ↑(fS sa) * (f r₁ * (↑(fS s₂)⁻¹ * f r₂))

Tactic:
← hf,

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₂
⊢ f ra * f r₂ = f ↑sa * (f r₁ * (↑(fS s₂)⁻¹ * f r₂))
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * (↑(fS s) * φ (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
← hf,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * (f ↑s * φ (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ pred^[b - a] b = a

Tactic:
Nat.pred_iterate,

Goal state after:
m n a b : ℕ
h : a ≤ b
⊢ b - (b - a) = a
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
⊢ x = x + 0

Tactic:
add_zero

Goal state after:
case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
⊢ x = x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ^[n + 1] x = x + ↑(n + 1)

Tactic:
Function.iterate_succ_apply',

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ (succ^[n] x) = x + ↑(n + 1)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred^[n + 1] x = x - ↑(n + 1)

Tactic:
Function.iterate_succ_apply',

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred (pred^[n] x) = x - ↑(n + 1)
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
x✝ : ℕ
⊢ ↑(↑x✝).toNat = ↑x✝ ↔ ↑x✝ ≠ ⊤

Tactic:
simp [toNat_natCast]

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:
replace h := congr($h.pred_eq.1)
    rw [coe_pred_of_mem nh] at h
    simp at h

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

Goal state before:
pp: case inr.inr
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
induction x with
      | top => simp [hy, this]
      | coe x =>
        induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -natCast_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b a : α
s : Sym α n
⊢ (a ::ₘ ↑s).card = n.succ

Tactic:
Multiset.card_cons,

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b a : α
s : Sym α n
⊢ (↑s).card + 1 = n.succ
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ ofFn v.get = v

Tactic:
by
  ext
  apply List.Vector.get_ofFn

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : n + 1 = (a ::ₘ m).card
⊢ m.card = n

Tactic:
Multiset.card_cons,

Goal state after:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : n + 1 = m.card + 1
⊢ m.card = n
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ count b ↑m + 0 = count b ↑m

Tactic:
add_zero

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ count b ↑m = count b ↑m
Module: Mathlib.Data.Sym.Basic

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

Tactic:
by
  by_cases h : none ∈ s
  · simp [h]
  · simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map,
      comp_apply, Option.some_get]
    convert! s.attach_map_coe

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x, f ↑x ⋯) * ∏ x, g ↑x ⋯ = (∏ a, f ↑a ⋯) * ∏ a, g ↑a ⋯

Tactic:
congr 1

Goal state after:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, f ↑x ⋯ = ∏ a, f ↑a ⋯

case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ (⋃ i, t i).Countable

Tactic:
by
  have := fun i ↦ (ht i).to_subtype
  rw [iUnion_eq_range_psigma]
  apply countable_range

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ s x a ↔ s x b

Tactic:
← hf,

Goal state after:
case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ x ∈ Set.range ⇑f ↔ s x b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f.top = g.top
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s g.top f.top
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
· let f := f.subrelIso
        rw [h] at f
        exact ⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s g.top f.top
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : o.get ⋯ = a
⊢ p ∧ ∃ h, o.get h = a

Tactic:
exact ⟨h₀, ⟨_, h₁⟩⟩

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

Goal state before:
pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
exact h₂.trans subset_succChain

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
s t : Set α
hst : s ⊆ t
⊢ (fun s ↦ (g '' (f '' s)ᶜ)ᶜ) s ⊆ (fun s ↦ (g '' (f '' s)ᶜ)ᶜ) t

Tactic:
dsimp at hst ⊢

Goal state after:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
s t : Set α
hst : s ⊆ t
⊢ (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ (x + y).toENatAux = ⊤

Tactic:
exact toENatAux_eq_top <| le_add_left hy

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a

Tactic:
exact a.isSMulRegular M

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ succ 0 ≤ c ↔ 0 < c

Tactic:
succ_le_iff

Goal state after:
c : Cardinal.{u_1}
⊢ 0 < c ↔ 0 < c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
by
  have : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0 := fun a => ne_bot_of_le_ne_bot aleph0_ne_zero a
  simp only [aleph0_le_mul_iff, and_or_left, and_iff_right_of_imp this, @and_left_comm (a ≠ 0)]
  simp only [and_comm, or_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩ = ⟨hM, ⟨hN, snd✝⟩⟩

Tactic:
congr 1

Goal state after:
case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = hM

case e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨hN, snd✝⟩
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
have : h • b ≠ 0 := by
    refine (ne_of_apply_ne (h⁻¹ • ·) ?_)
    simpa [this]

Goal state after:
case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h) • (a / b) = g • a / h • b
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
eq_div_iff_mul_eq this,

Goal state after:
case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h) • (a / b) * h • b = g • a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨hN, snd✝⟩

Tactic:
congr 1

Goal state after:
case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = hN

case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩ = ⟨fst✝, ⟨x, snd✝⟩⟩

Tactic:
congr 1

Goal state after:
case e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = fst✝

case e_4
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨x, snd✝⟩
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨x, snd✝⟩

Tactic:
congr 1

Goal state after:
case e_4.e_2
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x_1 ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

case e_4.e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = x

case e_4.e_4
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p

Tactic:
rw [← one_smul R x, ← smul_assoc]
  exact p.smul_mem _ h

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ (f ∘ₗ g).restrict ⋯ = (g ∘ₗ f).restrict ⋯

Tactic:
congr 1

Goal state after:
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
x✝ : R
⊢ x✝ • 1 = 1

Tactic:
by
      ext
      simp [smul_one]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
x : M × N
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (MulHom.fst M N) s

Tactic:
by simp [mem_prod, MulHom.coe_fst]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mem.one
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
⊢ p 1 z ⋯ ⋯

Tactic:
| one =>

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case one
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
⊢ p x 1 hx ⋯

Tactic:
| one =>

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.mem.one
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = 1

Tactic:
| one =>

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mem.one
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
⊢ p 1 z ⋯ ⋯

Tactic:
| one =>

Goal state after: