mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inl b) ↔ inl a ≤ inl b

Tactic:
change
          toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔
            toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)

Goal state after:
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ toLex (inr (toDual a)) ≤ toLex (inr (toDual b)) ↔ toDual (toLex (inl a)) ≤ toDual (toLex (inl b))
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
b : α ⊕ β
⊢ Sum.Lex r s b ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    b ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
cases b

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a val✝ : α
⊢ Sum.Lex r s (Sum.inl val✝) ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    Sum.inl val✝ ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
val✝ : β
⊢ Sum.Lex r s (Sum.inr val✝) ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    Sum.inr val✝ ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithBot α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b

Tactic:
cases b

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ ↑a✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithBot α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ b

Tactic:
cases b

Goal state after:
case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝¹, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithTop α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b

Tactic:
cases b

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ ↑a✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithTop α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝ ≤ b

Tactic:
cases b

Goal state after:
case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝ ≤ ⊤

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝¹, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ a' < a, f a' = b) → b < f a

Tactic:
rintro ⟨c, hc, rfl⟩
    exact f.strictMono hc

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : α
h : some x = none
⊢ False

Tactic:
exact true_ne_false (congr_arg Dom h)

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

Goal state before:
pp: case succ.inl
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
exact Or.inl (ih.trans subset_succChain)

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

Goal state before:
pp: case succ.inl
α : 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✝
hc₁ : ChainClosure r s✝
h : s✝ ⊆ SuccChain r s✝
h₁ : s✝ ⊆ s✝
⊢ SuccChain r s✝ ⊆ SuccChain r s✝

Tactic:
exact Subset.rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : 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 : ℕ
⊢ (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) i ≤
    (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))
      i

Tactic:
apply (f (c i)).monotone

Goal state after:
case a
α : 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 : ℕ
⊢ g (c.toOrderHom i) ≤ ωSup (c.map { toFun := g, monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i ∈ ∅, f i)

Tactic:
Finset.prod_empty,

Goal state after:
case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')

Tactic:
lift_iSup hf,

Goal state after:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ ⨆ i, lift.{w', w} (f i) ≤ lift.{w, w'} (iSup f')
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = lift.{u, 0} #(Fin n) ↔ Nonempty (α ≃ Fin n)

Tactic:
← lift_uzero #α,

Goal state after:
α : Type u
n : ℕ
⊢ lift.{0, u} #α = lift.{u, 0} #(Fin n) ↔ Nonempty (α ≃ Fin n)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ #α ≤ lift.{u, 0} #ℕ ↔ Nonempty (α ↪ ℕ)

Tactic:
← lift_uzero #α,

Goal state after:
α : Type u
⊢ lift.{0, u} #α ≤ lift.{u, 0} #ℕ ↔ Nonempty (α ↪ ℕ)
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
by
  let h := (@mul_lt_aleph0_iff a b).not
  rwa [not_lt, not_or, not_or, not_and_or, not_lt, not_lt] at h

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (m • f (g x)) = g (φ (φ' m) • f (g x))

Tactic:
rw [k]

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

Goal state before:
pp: case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)

Tactic:
by
  induction k with
  | zero => simp [one_eq_id]
  | succ k ih => rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]

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 : Submodule R M
x : M
⊢ x ∈ ⊥ → x ∈ p

Tactic:
simp +contextual [zero_mem]

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map (a • f) p ≤ map f p

Tactic:
by rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]

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₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q

Tactic:
simp only [SetLike.le_def, mem_comap, mem_inf, LinearMap.add_apply]

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₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄, f₁ x ∈ q ∧ f₂ x ∈ q → f₁ x + f₂ x ∈ q
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False

Tactic:
have :=
    NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
  rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this
  rcases this with (⟨_, h⟩ | ⟨h, _⟩)
  · exact zero_ne_one h.symm
  · exact zero_ne_one h.symm

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

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ (x - (algebraMap R A) r) * (x * (x - (algebraMap R A) r) ^ n) =
    (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n * x

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ (x - (algebraMap R A) r) * ((x - (algebraMap R A) r) ^ n * x) =
    (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n * x
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mem.mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ x✝ : R
h : x✝ ∈ s
⊢ x✝ ∈ closure s

Tactic:
exact subset_closure h

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

Goal state before:
pp: case mem.mem
R : Type u
inst✝ : NonAssocRing R
s : Set R
x✝¹ x x✝ : R
h : x✝ ∈ s
⊢ x✝ ∈ closure s

Tactic:
exact subset_closure h

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsLeft M₀ = nonZeroDivisorsLeft M₀ ⊓ nonZeroDivisorsRight M₀

Tactic:
nonZeroDivisorsLeft_eq_right,

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsRight M₀ = nonZeroDivisorsRight M₀ ⊓ nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x * a = 0

Tactic:
← Associates.mk_eq_zero,

Goal state after:
case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Associates.mk (x * a) = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

Tactic:
by
  simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]

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

Goal state before:
pp: case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ g ^ 0 • a

Tactic:
rw [pow_zero, one_smul]

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

Goal state before:
pp: case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g ^ 0 • a ≤ a

Tactic:
rw [pow_zero, one_smul]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
hx : x ∈ s • ⊥
⊢ x ∈ ⊥

Tactic:
induction x, hx using set_smul_inductionOn <;> aesop

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (a ⊔ b) ⊓ c ⊔ b ≤ b

Tactic:
hsup.eq_bot,

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ ⊥ ⊔ b ≤ b
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
hb : b ∈ span R t
⊢ p a b ha hb

Tactic:
induction hb using span_induction with

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ b ⊔ (d ⊔ a) ⊓ c = c

Tactic:
· simp [← sup_inf_assoc_of_le _ hc, ← sup_assoc, hcodisjoint.eq_top]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) → x ∈ p ⊔ p'

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
⊢ y + z ∈ p ⊔ p'
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom (u b) ↔ IsAtom b

Tactic:
← gi.isAtom_iff hbot h_atom,

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom (l (u b)) ↔ IsAtom b
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
have Sne : S.Nonempty := by
        suffices ⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
Sne : S.Nonempty
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
⊢ b₁ = b₂

Tactic:
by_contra h_ne

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
h_ne : ¬b₁ = b₂
⊢ False
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
⊢ s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f

Tactic:
by
  funext
  simp only [mulIndicator]
  split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
| ∏ x, (φ x) (mulSingle i m x) = (φ i) m

Tactic:
conv =>

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
j : ι
| mulSingle i (φ' i m) j