mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α β : Type u
f : F (α → β)
x : Unit → F α
⊢ s1 f x = s2 f x

Tactic:
exact H2 f (x Unit.unit)

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
n m : ℕ
v : Vector α m
⊢ (drop n v).toList = List.drop n v.toList

Tactic:
by
  cases v
  rfl

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
n m : ℕ
v : Vector α m
⊢ (take n v).toList = List.take n v.toList

Tactic:
by
  cases v
  rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j, if i = j then f j else 1) = f i

Tactic:
by
  rw [Finset.prod_ite_eq, if_pos (mem_univ _)]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v

Tactic:
by
  cases v
  rfl

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ (Set.image2 f s t).Countable

Tactic:
rw [← image_prod]
  exact (hs.prod ht).image _

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simpa using fun h ↦ ha <| trans h hb

Goal state after:
case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩
  by_contra hx
  rw [← h] at hx
  simpa [h] using csSup_mem_of_not_isSuccPrelimit hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsUpperSet s
⊢ s = ∅ ∨ ∃ a, s = Ici a

Tactic:
by
  refine or_iff_not_imp_left.2 fun ha ↦ ?_
  obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 ha
  exact ⟨_, ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2

Tactic:
· rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq]
      intro _ hb
      exact (hp _ hb).2

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ Function.Injective fun c ↦ ⇑c.toOrderHom

Tactic:
rintro ⟨f, hf⟩

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : ℕ → α
hf : Monotone f
⊢ ∀ ⦃a₂ : Chain α⦄,
    (fun c ↦ ⇑c.toOrderHom) { toFun := f, monotone' := hf } = (fun c ↦ ⇑c.toOrderHom) a₂ →
      { toFun := f, monotone' := hf } = a₂
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ChainClosure r ∅

Tactic:
have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => (notMem_empty _ h).elim

Goal state after:
α : Type u_1
r : α → α → Prop
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
hz' : z ∈ bot x f
⊢ f z ≤ f y

Tactic:
rw [← bot_eq_of_le_or_map_le le_map hy] at hz'

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
hz' : z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ f z ≤ f y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.isTrue
α : 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
this : Injective h
a : α
h✝ : a ∈ s
⊢ R a (f a)

Tactic:
exact hp₁ a

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ sum (f + g) = sum f + sum g

Tactic:
have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
  simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this
  exact this

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

Goal state before:
pp: α β : Type u
f : α ↪ β
s : Set α
⊢ #↑(⇑f '' s) = #↑s

Tactic:
by
  simpa using mk_image_embedding_lift f s

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

Goal state before:
pp: α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x ∈ s, A x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)

Tactic:
by
  rw [biUnion_eq_iUnion]
  apply mk_iUnion_le_lift

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

Goal state before:
pp: α : Type u
s : Set α
a : α
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
by
  by_cases h : a ∈ s
  · simp only [insert_eq_of_mem h, self_le_add_right]
  · rw [mk_insert h]

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

Goal state before:
pp: M : Type u_1
β : Type u_4
inst✝³ : SMul M β
α : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)

Tactic:
Prod.smul_mk,

Goal state after:
M : Type u_1
β : Type u_4
inst✝³ : SMul M β
α : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ (a • 0, a • c) = (0, a • c)
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝³ : SMul M α
β : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ a • (b, 0) = (a • b, 0)

Tactic:
Prod.smul_mk,

Goal state after:
M : Type u_1
α : Type u_3
inst✝³ : SMul M α
β : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ (a • b, a • 0) = (a • b, 0)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
⊢ { toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) c • { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext
    apply mul_smul

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ⋂ i, ↑(p i) ↔ ∀ (i : ι), x ∈ p i

Tactic:
Set.mem_iInter

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i
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 σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
S : Submodule R M
x : M
⊢ ∀ x_1 ∈ S, f x_1 = f x → x ∈ S

Tactic:
intro y hy hxy

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 σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
S : Submodule R M
x y : M
hy : y ∈ S
hxy : f y = f x
⊢ x ∈ S
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ Disjoint p q ↔ p ⊓ q = ⊥

Tactic:
disjoint_iff

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ p ⊓ q = ⊥ ↔ p ⊓ q = ⊥
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₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective ⇑f
y : ↥q
⊢ ∃ a, (f.submoduleComap q) a = y

Tactic:
by
  obtain ⟨x, hx⟩ := hf y
  use ⟨x, Submodule.mem_comap.mpr (hx ▸ y.2)⟩
  apply Subtype.val_injective
  simp [hx]

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
by ext <;> exact left_distrib ..

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul.add_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_add] using add_mem h₁ h₂

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

Goal state before:
pp: case mul.add_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa [mul_add] using add_mem h₁ h₂

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a' b' c' : Associates M
a b c : M
⊢ ⟦a * b * c⟧ = ⟦a * (b * c)⟧

Tactic:
rw [mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p m : Associates M
hp : Prime p
hle : m ≤ p
⊢ m = 1 ∨ m = p

Tactic:
rcases mk_surjective p with ⟨p, rfl⟩

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
m : Associates M
p : M
hp : Prime (Associates.mk p)
hle : m ≤ Associates.mk p
⊢ m = 1 ∨ m = Associates.mk p
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
r : S
⊢ {r} • N = r • N

Tactic:
apply set_smul_eq_of_le

Goal state after:
case closed_under_smul
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
r : S
⊢ ∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N

case le
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
r : S
⊢ r • N ≤ {r} • N
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
x✝ : M
hx✝ : x✝ ∈ closure (univ • s)
r : R
x : M
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 • x2) r x ∈ ↑(span R s).toAddSubmonoid

Tactic:
exact smul_mem _ _ (subset_span hx)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', Disjoint a a' ∧ a ⊔ a' = b

Tactic:
disjoint_iff

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', a ⊓ a' = ⊥ ∧ a ⊔ a' = 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 : Submodule R M
v₀ : M
⊢ s ≤ R ∙ v₀ ↔ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
simp_rw [SetLike.le_def, mem_span_singleton]

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
⊢ R ∙ x = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v

Tactic:
rw [eq_top_iff, le_span_singleton_iff]
  tauto

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteLattice α
⊢ IsAtomistic α ↔ ∀ (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]

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
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif g c then c else cᶜ) → c = ⊥

Tactic:
cases g c <;> simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]
  exact hs.sSup_mem_of_nonempty (ht.image _) (by simpa) (by simpa)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
hbot : x ⊓ a = ⊥
⊢ x ≤ a

Tactic:
exact False.elim <| hcon <|
        (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
i : ι
s : Finset ι
f : ι → α
hs : s.SupIndep f
h : Disjoint (f i) (s.sup f)
⊢ (insert i s).SupIndep f

Tactic:
grind [insert_eq, SupIndep.union, sup_singleton]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
rw [ht₂]
    exact hsc.finsetSup_mem h ht₁

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

Tactic:
by
  simp_rw [inf_comm _ a, h.inf_sSup_eq]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i✝ : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i✝}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' ↑t
j : ι
x✝ : j ∈ f ⁻¹' ↑t
hij : f i = f j
⊢ i ∈ {i | f i ≠ ⊥}

Tactic:
aesop (add norm simp [t])

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i✝ : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i✝}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' ↑t
j : ι
x✝ : j ∈ f ⁻¹' ↑t
hij : f i = f j
⊢ j ∈ {i | f i ≠ ⊥}

Tactic:
aesop (add norm simp [t])

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i✝ : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i✝}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' ↑t
j : ι
x✝ : j ∈ f ⁻¹' ↑t
hij : f i = f j
⊢ i ∈ {i | f i ≠ ⊥}

Tactic:
aesop (add norm simp [t])

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i✝ : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i✝}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' ↑t
j : ι
x✝ : j ∈ f ⁻¹' ↑t
hij : f i = f j
⊢ j ∈ {i | f i ≠ ⊥}

Tactic:
aesop (add norm simp [t])

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

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

Tactic:
rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]

Goal state after:
case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(span R s)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
le : comap f q ≤ p
⊢ comap f (map f p ⊔ q) = p

Tactic:
by
  refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)
  obtain ⟨_, ⟨y, hy, rfl⟩, z, hz, eq⟩ := mem_sup.mp h
  rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq; subst eq
  simpa using p.add_mem (le hz) hy

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ IsCompl s (K ∙ x)

Tactic:
refine ⟨disjoint_span_singleton_of_notMem hx, ?_⟩

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ Codisjoint s (K ∙ x)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, ((-1) ^ #t * ∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i

Tactic:
simp [sub_eq_neg_add, prod_add, prod_neg, mul_right_comm]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : IsOrderedMonoid α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
x : α
hx : x ∈ ⟦l⟧
⊢ x ≤ prod ⟦l⟧

Tactic:
by simpa using List.single_le_prod hl x hx

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
⊢ ∏ i ∈ s, f i < ∏ i ∈ s, g i

Tactic:
← insert_erase hi,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
⊢ ∏ i ∈ insert i (s.erase i), f i < ∏ i ∈ insert i (s.erase i), g i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' ↑x.support
⊢ ∀ x_1 ∈ x.support, (single (f x_1) (x x_1)) b = 0

Tactic:
exact fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' ↑(single b m).support)
⊢ comapDomain f (single b m) hf = 0

Tactic:
by
  classical
  ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb

Goal state after: