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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithBot α
⊢ 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 a <;> 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✝

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: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithTop α
⊢ ((Equiv.optionEquivSumPUnit α).trans toLex) a ≤ ((Equiv.optionEquivSumPUnit α).trans toLex) b ↔ a ≤ b

Tactic:
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Lex.toLex_le_toLex, le_refl]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithTop α
⊢ 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
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithTop α
⊢ 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 a <;> 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✝

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.Part

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
β γ : Type u_4
f : α → Part (β → γ)
g : α → Part β
hf : Monotone f
hg : Monotone g
⊢ Monotone fun x ↦ f x <*> g x

Tactic:
simpa only [seq_eq_bind_map] using! hf.partBind <| Monotone.of_apply₂ fun _ ↦ hg.partMap

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o

Tactic:
exact mt Exists.fst h

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ≤ y ∨ f y ≤ x

Tactic:
· exact Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ y ∈ ωSup (c.map g) b

Tactic:
apply le_ωSup (c.map g) _ _ _ hb₁

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

Goal state before:
pp: case mk
α : Type u
⊢ ¬#(Set α) ≤ #α

Tactic:
rintro ⟨⟨f, hf⟩⟩

Goal state after:
case mk
α : Type u
f : Set α → α
hf : Injective f
⊢ False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b : Cardinal.{u_1}
h : a < b
⊢ a + 1 ≤ b

Tactic:
induction a, b using Cardinal.inductionOn₂ with | mk α β

Goal state after:
case mk
α β : Type u_1
h : #α < #β
⊢ #α + 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

Goal state after:
d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
⊢ toNat (↑c + d) = toNat ↑c + toNat d
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ ↑(toNat c) ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d

Tactic:
← cast_toNat_of_lt_aleph0 (not_le.mp hd)

Goal state after:
case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ ↑(toNat c) ↔ ↑n ≤ ↑(toNat d)
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : ↑x ≤ y
⊢ (↑x * y).toENatAux = (↑x).toENatAux * y.toENatAux

Tactic:
lift y to ℕ using hy

Goal state after:
case inl
x y : ℕ
hle : ↑x ≤ ↑y
⊢ (↑x * ↑y).toENatAux = (↑x).toENatAux * (↑y).toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
lift y to ℕ using hy

Goal state after:
case inl
x y : ℕ
hle : ↑x ≤ ↑y
⊢ (↑x + ↑y).toENatAux = (↑x).toENatAux + (↑y).toENatAux
Module: Mathlib.Algebra.Module.RingHom

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
a b : R
x : M
⊢ (f a + f b) • x = f a • x + f b • x

Tactic:
by simp only [← f.map_add, hsmul, add_smul]

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = (ψ ∘ φ) x

Tactic:
Function.comp_apply

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = ψ (φ x)
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 b : M
ab : (fun x ↦ 1 • x) a = (fun x ↦ 1 • x) b
⊢ a = b

Tactic:
dsimp only [Function.comp_def] at ab

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b
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 ↔ Nontrivial M

Tactic:
nontrivial_iff,

Goal state after:
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
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∃ n, c = ↑n

Tactic:
rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩

Goal state after:
c : Cardinal.{0}
h' : c < #ℕ
h : lift.{u_1, 0} c < ℵ₀
⊢ ∃ n, lift.{u_1, 0} c = ↑n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
this : S.Finite
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
lift S to Finset ℕ using this
      simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
by
  rw [image_eq_range] at h
  convert! mk_preimage_of_subset_range_lift _ _ h using 1
  rw [mk_sep]
  rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝³ : SMul M X
inst✝² : SMul N Y
inst✝¹ : SMul R Y
inst✝ : SMulCommClass N R Y
h : R
f : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (h • ⇑f) (m • x) = σ m • (h • ⇑f) x

Tactic:
simp [smul_comm _ h]

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✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker = ⊥ ↔ Injective ⇑f

Tactic:
by
  simpa [disjoint_iff_inf_le] using disjoint_ker_iff_injOn (f := f) (p := ⊤)

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)

Tactic:
rw [mul_zero, mul_zero, mul_zero]

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ r • s • a = s • r • a

Tactic:
by
    rw [Algebra.smul_def, mul_smul_comm, ← Algebra.smul_def]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsDomain A
⊢ IsTorsionFree R A ↔ Injective ⇑(algebraMap R A)

Tactic:
by
  rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a

Tactic:
exact hp.pow_dvd_of_dvd_mul_left n h h'

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a

Tactic:
rw [mul_comm] at h'
  exact hp.pow_dvd_of_dvd_mul_left n h h'

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
c : M
⊢ a * c ~ᵤ b * c

Tactic:
by
  obtain ⟨d, rfl⟩ := h; exact ⟨d, mul_right_comm _ _ _⟩

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑(unitsNonZeroDivisorsEquiv.symm.symm b_1) = ↑b) ↔ Associated a b

Tactic:
simp [Associated]

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ¬IsUnit x

Tactic:
contrapose ndvd

Goal state after:
case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : IsUnit x
⊢ a * x ∣ a
Module: Mathlib.Algebra.Module.Submodule.Equiv

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩

Tactic:
have : ⟨f y, LinearMap.mem_range_self f y⟩ = LinearEquiv.ofInjective f h y := rfl

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
this : ⟨f y, ⋯⟩ = (ofInjective f h) y
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]

Goal state after:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2) ↔ (∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2
Module: Mathlib.Order.ModularLattice

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

Tactic:
by
  rw [disjoint_comm, sup_comm]
  apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm
  rwa [sup_comm, disjoint_comm] at hsup

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : IsModularLattice α
a b c : α
inst✝² : BoundedOrder α
inst✝¹ : ComplementedLattice α
inst✝ : Fact (a ≤ b)
x✝ : ↑(Icc a b)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ b_1, x ⊓ ↑b_1 = a ∧ x ⊔ ↑b_1 = b

Tactic:
obtain ⟨y, rfl, rfl⟩ := exists_inf_eq_and_sup_eq ha hb

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : IsModularLattice α
c : α
inst✝² : BoundedOrder α
inst✝¹ : ComplementedLattice α
x y : α
ha : x ⊓ y ≤ x
hb : x ≤ x ⊔ y
inst✝ : Fact (x ⊓ y ≤ x ⊔ y)
x✝ : ↑(Icc (x ⊓ y) (x ⊔ y))
⊢ ∃ b, x ⊓ ↑b = x ⊓ y ∧ x ⊔ ↑b = x ⊔ y
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 : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ r • ↑(f 1) = x

Tactic:
rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]

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 y z : M
a b c : R
⊢ a • x + b • y + c • z = a • x + (b • y + c • z)

Tactic:
rw [add_assoc]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
⊢ (image g s).SupIndep f

Tactic:
intro t ht i hi hit
  rcases subset_image_iff.mp ht with ⟨t, hts, rfl⟩
  rcases mem_image.mp hi with ⟨i, his, rfl⟩
  rw [sup_image]
  exact hs hts his (hit <| mem_image_of_mem _ ·)

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ False

Tactic:
apply hj

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j = ⊥
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : One M
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x

Tactic:
let := Classical.decPred (· ∈ s)
  convert! s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
n : ℕ
hn : a n = sSup (range ⇑a)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
refine ⟨n, fun m hm ↦ ?_⟩

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
n : ℕ
hn : a n = sSup (range ⇑a)
m : ℕ
hm : n ≤ m
⊢ ¬a n < a m
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ⟨hts, htsup⟩⟩ := h s

Goal state after:
case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ span S (range ⇑(inclusion h₁)) = ⊤

Tactic:
suffices (span S (range (inclusion h₁))).map q.subtype = q by
    apply map_injective_of_injective q.injective_subtype
    rw [this, q.map_subtype_top]

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ map q.subtype (span S (range ⇑(inclusion h₁))) = q
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
a : List α
l : List (List α)
⊢ ((↑a).bind fun a ↦ map (cons a) (↑(List.map (fun l ↦ ↑l) l)).Sections) =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))

Tactic:
bind_map_comm,

Goal state after:
α : Type u_1
a : List α
l : List (List α)
⊢ ((↑(List.map (fun l ↦ ↑l) l)).Sections.bind fun b ↦ map (fun a ↦ a ::ₘ b) ↑a) =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
y : M'
hy : y ∈ q₁
y' : M'
hy' : y' ∈ q₁'
hyy : y + y' ∈ q₁ ⊔ q₁'
⊢ (x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
exact mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (sSup '' c)

Tactic:
directedOn_image

Goal state after:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ DirectedOn (sSup ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) c
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (sSup '' c)

Tactic:
rw [directedOn_image]

Goal state after:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ DirectedOn (sSup ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) c
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f

Tactic:
by
  rw [mulIndicator_sdiff h, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
⊢ optionElim (i + j) (a + b) = optionElim i a + optionElim j b

Tactic:
ext x; cases x <;> simp

Goal state after: