mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ ≤ b * ↑x

Tactic:
bot_le

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
⊢ a * x ≤ b * x

Tactic:
by
    rcases eq_or_ne x 0 with rfl | x0'
    · simp
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
    cases a
    · simp_rw [bot_mul x0', bot_le]
    cases b
    · exact absurd h (bot_lt_coe _).not_ge
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact mul_le_mul_of_nonneg_right h x0

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ^[n.succ] a ≤ succ^[m] a

Tactic:
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
h_le : n + 1 ≤ m
⊢ succ^[n.succ] a ≤ succ^[m] a
Module: Mathlib.Order.SuccPred.Limit

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

Tactic:
rw [prelimitRecOn, WellFounded.fix_eq, dif_neg h]

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ cast ⋯
      (succ (Classical.choose ⋯) ⋯
        ((fun y x ↦
            ⋯.fix
              (fun a IH ↦
                if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    succ b hb (prelimitRecOn b succ isSuccPrelimit)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ y - 1 ↔ x < y

Tactic:
rw [← pred_eq_sub_one, le_pred_iff_of_not_isMin hy]

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

Goal state before:
pp: n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ 0 < n.toNat

Tactic:
pos_iff_ne_zero,

Goal state after:
n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ n.toNat ≠ 0
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩

Tactic:
dsimp only

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ ⟨b, hb⟩ ≤ if h : pred c ∈ s then ⟨pred c, h⟩ else ⟨c, hc⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
⊢ x = default

Tactic:
have := x.val_inv
    have x_top : x.val ≠ ⊤ := by
      intro h
      simp [h] at this
    have x_inv_top : x.inv ≠ ⊤ := by
      intro h
      simp only [h, ne_eq, x.ne_zero, not_false_eq_true, mul_top, top_ne_one] at this
    obtain ⟨y, x_y⟩ := ne_top_iff_exists.1 x_top
    obtain ⟨z, x_z⟩ := ne_top_iff_exists.1 x_inv_top
    replace x_y := x_y.symm
    rw [x_y, ← x_z, ← natCast_mul, ← natCast_one, natCast_inj, _root_.mul_eq_one] at this
    rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y

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

Goal state before:
pp: n : ℕ
m : WithBot ℕ∞
⊢ ↑n + 1 ≤ m ↔ ↑n < m

Tactic:
rw [← WithBot.coe_one, ← natCast_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]

Goal state after:
n : ℕ
m : WithBot ℕ∞
⊢ ↑↑(n + 1) ≤ m ↔ ↑n < m
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
← piecewise_coe

Goal state after:
ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ (↑s).piecewise f g ∈ t.pi t'
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map coeEmb.toEmbedding Finset.univ

Tactic:
classical
    refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
    simp

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
⊢ (↑s).card + 1 = n.succ

Tactic:
s.2

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

Goal state before:
pp: α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
⊢ Countable ((a : α) → π a)

Tactic:
have f := fun a => (nonempty_embedding_nat (π a)).some

Goal state after:
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
f : (a : α) → π a ↪ ℕ
⊢ Countable ((a : α) → π a)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b

Tactic:
have : v = nil := by simp only [eq_iff_true_of_subsingleton]

Goal state after:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
this : v = nil
⊢ (scanl f b v).head = b
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite

Tactic:
· exact infinite_range_of_injective <| Injective.comp Subtype.val_injective hf

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ BddAbove s

Tactic:
contrapose! hlim

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit (sSup s)
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun i ↦ f (i + 1)

Tactic:
refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_

Goal state after:
f : ℕ → Cardinal.{u}
⊢ #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i ↦ f (i + 1)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(have H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x ↦
                      IsWellFounded.fix r
                        (fun a IH ↦
                          have H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH ↦
                  have H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}

Tactic:
dsimp only

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ⋯.min
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s (↑(IsWellFounded.fix r (fun a IH ↦ ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩) a_1))
              b}
      ⋯ ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s (↑(IsWellFounded.fix r (fun a IH ↦ ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩) a')) b}
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(have H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x ↦
                        IsWellFounded.fix r
                          (fun a IH ↦
                            have H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)

Tactic:
dsimp only

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (⋯.min
        {b |
          ∀ (a_1 : α),
            r a_1 a →
              s
                (↑(IsWellFounded.fix r (fun a IH ↦ ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                    a_1))
                b}
        ⋯)
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₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
⊢ False

Tactic:
obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃

Goal state after:
case union.inl
α : 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✝
h : SuccChain r c₃ ⊆ c₁
⊢ False

case union.inr
α : 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✝
h : c₁ ⊆ c₃
⊢ False
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ ⦃y : α⦄, (fun x_1 ↦ x_1 ∈ {y | y ∈ s ∧ x ≤ y}) y → m ≤ y → y ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x ↦ x ∈ s) m

Tactic:
exact ⟨m, hxm, hms, fun z hzs hmz => @hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂

Tactic:
induction hc₂ generalizing c₁ hc₁ with

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂

Tactic:
induction hc₁ with
  | succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
  | union _ ih => exact sUnion_subset ih

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (max i j))
hy : y ∈ g (c (max i j)) b
⊢ y ∈ x

Tactic:
apply h''' (max i j)

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (max i j))
hy : y ∈ g (c (max i j)) b
⊢ y ∈ (c.map (f.partBind g)) (max i j)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
⊢ lift.{u, v} ↑n = ↑n

Tactic:
induction n

Goal state after:
case zero
⊢ lift.{u, v} ↑0 = ↑0

case succ
n✝ : ℕ
a✝ : lift.{u, v} ↑n✝ = ↑n✝
⊢ lift.{u, v} ↑(n✝ + 1) = ↑(n✝ + 1)
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ toNat (c + d) = toNat c + toNat d

Tactic:
lift c to ℕ using hc
  lift d to ℕ using hd
  norm_cast

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ ¬IsSMulRegular M 0 ↔ ∃ x y, x ≠ y

Tactic:
not_iff_comm,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ IsSMulRegular M 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} ↑univ
⊢ False

Tactic:
← bddAbove_iff_small

Goal state after:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
⊢ #↑(S ∪ T) + #↑(S ∩ T) = #↑S + #↑T

Tactic:
by
  classical
  exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

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
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
⊢ (fun _insts ↦
        have this := ⋯;
        prodOfSMulCommClass M N α)
      ((fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩)
        { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }) =
    { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }

Tactic:
dsimp only

Goal state after:
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
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
⊢ prodOfSMulCommClass M N α = { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }
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 α
⊢ (fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩)
      ((fun _insts ↦
          have this := ⋯;
          prodOfSMulCommClass M N α)
        ⟨hM, ⟨hN, snd✝⟩⟩) =
    ⟨hM, ⟨hN, snd✝⟩⟩

Tactic:
dsimp only

Goal state after:
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✝⟩⟩
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 α
x✝ : DistribMulAction (M × N) α
⊢ (fun _insts ↦
        have this := ⋯;
        prodOfSMulCommClass M N α)
      ((fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩) x✝) =
    x✝

Tactic:
dsimp only

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
⊢ prodOfSMulCommClass M N α = x✝
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 α
⊢ (fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩)
      ((fun _insts ↦
          have this := ⋯;
          prodOfSMulCommClass M N α)
        ⟨fst✝, ⟨x, snd✝⟩⟩) =
    ⟨fst✝, ⟨x, snd✝⟩⟩

Tactic:
dsimp only

Goal state after:
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✝⟩⟩
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 α
m : M
a : α
| SMul.smul m a

Tactic:
rw [← one_smul N a]

Goal state after:
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 α
m : M
a : α
| SMul.smul m (1 • a)
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋂ s ∈ S, ↑s → c • x ∈ ⋂ s ∈ S, ↑s

Tactic:
by simp +contextual [smul_mem]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑p ∩ ↑q → c • x ∈ ↑p ∩ ↑q

Tactic:
by simp +contextual [smul_mem]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
· rw [Finset.inf_insert, coe_inf, ih]
    simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : sSup s = ⊤
⊢ ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0

Tactic:
by
  contrapose! h
  simp_rw [← ker_eq_top, eq_top_iff, ← hs, sSup_le_iff, le_ker_iff_comp_subtype_eq_zero]
  exact h

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
h : comap f q < p
⊢ q < map f p

Tactic:
rw [lt_iff_le_not_ge] at h ⊢

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n : ℕ
⊢ ↑n ∈ s

Tactic:
induction n

Goal state after:
case zero
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
⊢ ↑0 ∈ s

case succ
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n✝ : ℕ
a✝ : ↑n✝ ∈ s
⊢ ↑(n✝ + 1) ∈ s
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).1 = ↑n

Tactic:
induction n

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).1 = ↑0

case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).1 = ↑n✝
⊢ (↑(n✝ + 1)).1 = ↑(n✝ + 1)
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).2 = ↑n

Tactic:
induction n

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).2 = ↑0

case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).2 = ↑n✝
⊢ (↑(n✝ + 1)).2 = ↑(n✝ + 1)
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Tactic:
refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
⊢ C x₂
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: case mem
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r : R
hr : r ∈ ↑S
⊢ r * b ∈ closure ↑S

Tactic:
exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x✝

Tactic:
| neg _ _ hL =>

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u.isUnit_units_mul]

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit (↑u * A) ∨ IsUnit B
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_1
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
⊢ Irreducible x

Tactic:
rwa [irreducible_mul_isUnit h'] at h

Goal state after: