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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (map f x).bind g = x.bind fun y ↦ g (f y)

Tactic:
by rw [← bind_some_eq_map, bind_assoc]; simp

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i
this : ∃ x_1, ¬c x_1 ≤ x
⊢ ∃ i, ¬c i ≤ x

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f = ⨆ n, (⇑f)^[n] ⊥

Tactic:
apply le_antisymm
  · apply lfp_le_fixed
    exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)
  · apply le_lfp
    intro a h_a
    exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr
α : 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
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ z_1 ∈ c, z_1 ≤ z
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
g : α → β
hg : ωScottContinuous g
f : α → β
hf : ωScottContinuous f
⊢ ωScottContinuous f

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous g

Tactic:
assumption

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

Goal state before:
pp: case refine_1
α : 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 β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : g' (g x') = g' (g y')
⊢ g x' = g y'

Tactic:
g'g _,

Goal state after:
case refine_1
α : 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 β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = g' (g y')
⊢ g x' = g y'
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
subst x
              exact fun e => (hf i y hy e.symm).elim

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 b : M
ab : a = b
⊢ a = b

Tactic:
assumption

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

Goal state before:
pp: ⊢ ℵ₀.IsStrongLimit

Tactic:
refine ⟨aleph0_ne_zero, fun x hx ↦ ?_⟩

Goal state after:
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ 2 ^ x < ℵ₀
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁶ : Monoid S'
inst✝⁵ : DistribMulAction S' M
inst✝⁴ : SMulCommClass R S' M
inst✝³ : Monoid T'
inst✝² : DistribMulAction T' M
inst✝¹ : SMulCommClass R T' M
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ (s • t • f) m = (t • s • f) m

Tactic:
DomMulAct.smul_linearMap_apply,

Goal state after:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁶ : Monoid S'
inst✝⁵ : DistribMulAction S' M
inst✝⁴ : SMulCommClass R S' M
inst✝³ : Monoid T'
inst✝² : DistribMulAction T' M
inst✝¹ : SMulCommClass R T' M
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ f (DomMulAct.mk.symm t • DomMulAct.mk.symm s • m) = f (DomMulAct.mk.symm s • DomMulAct.mk.symm t • m)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹) x✝ + (x✝² • x✝¹) x✝

Tactic:
DomMulAct.smul_linearMap_apply,

Goal state after:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm (x✝³ + x✝²) • x✝) = x✝¹ (DomMulAct.mk.symm x✝³ • x✝) + x✝¹ (DomMulAct.mk.symm x✝² • x✝)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ x ∈ p

Tactic:
rw [← neg_neg x]
    exact neg_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
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
⊢ g ^ k = 0

Tactic:
by
  ext m
  have hg : N.subtype.comp (g ^ k) m = 0 := by
    rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
  simpa using hg

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
m✝ : R
x✝ : ↥p
⊢ (Equiv.Set.image (⇑f) (↑p) i).toFun (m✝ • x✝) = σ₁₂ m✝ • (Equiv.Set.image (⇑f) (↑p) i).toFun x✝

Tactic:
simp only [coe_smul_of_tower, map_smulₛₗ _, Equiv.toFun_as_coe, Equiv.Set.image_apply]

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
m✝ : R
x✝ : ↥p
⊢ ⟨σ₁₂ m✝ • f ↑x✝, ⋯⟩ = σ₁₂ m✝ • ⟨f ↑x✝, ⋯⟩
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² : A →ₐ[R] A
x✝¹ x✝ : Aˣ
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
by ext; exact map_mul _ _ _

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

Goal state before:
pp: case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

Tactic:
assumption

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

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = p * (a * x)
⊢ p ∣ a ∨ a ∣ b

Tactic:
mul_right_inj' hp.ne_zero

Goal state after:
case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
⊢ p ≠ q

Tactic:
by_contra hcontra
  obtain ⟨hp, x, hx', hx''⟩ := h
  simp_all

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

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

Tactic:
nonZeroDivisorsLeft_eq_nonZeroDivisors

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ M₀⁰ ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsRight M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ M₀⁰ ∧ b ∈ M₀⁰

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀ ∧ b ∈ nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑(a * c)

Tactic:
Submonoid.coe_mul,

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑a * ↑c
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ ↑b = ↑(a * ⟨c, ⋯⟩)

Tactic:
Submonoid.coe_mul,

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ ↑b = ↑a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
⊢ ∀ {a : Associates M}, a ≠ 0 → IsLeftRegular a

Tactic:
rintro ⟨a⟩ ha ⟨b⟩ ⟨c⟩ h
      rcases Quotient.exact' h with ⟨u, hu⟩
      have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
      exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ p.subtype ⟨val✝, h⟩ ∈ p

Tactic:
assumption

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

Goal state before:
pp: case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ ⟨p.subtype ⟨val✝, h⟩, ⋯⟩ ∈ q

Tactic:
assumption

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
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x✝ : M
hx✝ : x✝ ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ {a} • N
⊢ x ∈ a • N

Tactic:
← Submodule.singleton_set_smul

Goal state after:
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
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x✝ : M
hx✝ : x✝ ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ {a} • N
⊢ x ∈ {a} • N
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝³ : PartialOrder α✝
α : Type u_4
a b : α
inst✝² : Preorder α
inst✝¹ : IsStronglyAtomic α
s : Set α
inst✝ : s.OrdConnected
⊢ s.OrdConnected

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyCoatomic α
s : Set α
h : s.OrdConnected
⊢ s.OrdConnected

Tactic:
assumption

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := ⋯
⊢ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p

Tactic:
sSup_le_iff

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
⊢ ∀ b ∈ {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}, b ≤ p
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
hbS : a ∈ S
hba : a ≤ a
⊢ a ∈ S

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ x

Tactic:
rcases eq_bot_or_eq_top x with (rfl | rfl)
        · rw [if_pos h]
        · exact le_top

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

Goal state before:
pp: case refine_1.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ update v j (v j + r • v i) k ∈ span R (range v)

Tactic:
exact subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
⊢ ∃ a, ⊤ = R ∙ a

Tactic:
refine ⟨⟨a, ha ▸ mem_span_singleton_self a⟩, .symm <| top_unique fun x _ ↦ ?_⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
x✝ : x ∈ ⊤
⊢ x ∈ R ∙ ⟨a, ⋯⟩
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ a' = ⊥

Tactic:
simpa using Subtype.coe_inj.2 ha'.inf_eq_bot

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsCoatom s ↔ ∃ x, s = {x}ᶜ

Tactic:
isCompl_compl.isCoatom_iff_isAtom,

Goal state after:
α : Type u_2
s : Set α
⊢ IsAtom sᶜ ↔ ∃ x, s = {x}ᶜ
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = ((algebraMap S A).comp (algebraMap R S)) x

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
⊢ False

Tactic:
replace h₁ : Disjoint (f i) (⨆ i ∈ s, f i) := (h₁ i).mono_right <| biSup_mono <| by aesop

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
h₁ : Disjoint (f i) (⨆ i ∈ s, f i)
⊢ False
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case a
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s ≤ t.sup id

Tactic:
assumption

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

Goal state before:
pp: case a
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ t.sup id ≤ sSup s

Tactic:
assumption

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
x : α
hx : x ∈ t
⊢ x ≤ sSup s

Tactic:
exact le_sSup (hts hx)

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : ¬a ∈ s
⊢ r 1 1

Tactic:
exacts [ha has, h1]

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

Goal state before:
pp: case mpr.smul
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ : M
a : R
x : M
hx : x ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ f ⟨a • x, ⋯⟩ = g ⟨a • x, ⋯⟩

Tactic:
| smul a x hx hx' =>

Goal state after:
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
S : Finset M
⊢ IsCompactElement (span R ↑S)

Tactic:
rw [span_eq_iSup_of_singleton_spans]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ IsCompactElement (⨆ x ∈ ↑S, R ∙ x)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ ⊥
⊢ False

Tactic:
exact ne_of_lt con (Subtype.ext_iff.1 (eq_top_of_isCompl_bot hc))

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

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ False

Tactic:
apply ha.1

Goal state after:
case inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a = ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
⊢ sSup {a | a ≤ c ∧ IsAtom a} ≤ b ⊔ sSup s

Tactic:
sSup_le_iff

Goal state after:
case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
⊢ ∀ b_1 ∈ {a | a ≤ c ∧ IsAtom a}, b_1 ≤ b ⊔ sSup s