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

Goal state before:
pp: α : Type u_1
inst✝¹ : ChainCompletePartialOrder α
f : α → α
inst✝ : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := ⋯
y : α := ⋯
⊢ f y ∈ bot x f

Tactic:
apply (bot_isAdmissible le_map).image_self_subset_self

Goal state after:
α : Type u_1
inst✝¹ : ChainCompletePartialOrder α
f : α → α
inst✝ : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := ⋯
y : α := ⋯
⊢ f y ∈ f '' bot x f
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c c' : Cardinal.{u_1}
⊢ c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')

Tactic:
conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

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 ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))

Tactic:
apply le_ωSup_of_le i

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 : ℕ
⊢ (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
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 : ℕ
⊢ g (c.toOrderHom i) ≤ ωSup (c.map { toFun := g, monotone' := ⋯ })

Tactic:
apply le_ωSup_of_le i

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) ≤ (c.map { toFun := g, monotone' := ⋯ }) i
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
⊢ (ωSup c₀) (ωSup c₁) = Prod.apply (ωSup (c₀.zip c₁))

Tactic:
by simp [Prod.apply_apply, Prod.ωSup_zip]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

pp: case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
· apply le_trans h
      change ((iterateChain f x h).map f) 0 ≤ ωSup ((iterateChain f x h).map (f : α →o α))
      apply le_ωSup

Goal state after:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

pp: x y : Cardinal.{u}
hle : x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
· rw [add_comm, this y x (le_of_not_ge hle), add_comm]

Goal state after:
x y : Cardinal.{u}
hle : x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ↑(toENat a) = a ↔ a ≤ ℵ₀

Tactic:
rw [eq_comm, ← enat_gc.exists_eq_l]

Goal state after:
a : Cardinal.{u_1}
⊢ (∃ b, a = ↑b) ↔ a ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)

Goal state after:
case refine_1
α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ⊢ ¬Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}

Tactic:
intro h
  have := small_lift.{_, v} Cardinal.{max u v}
  rw [← small_univ_iff, ← bddAbove_iff_small] at this
  exact not_bddAbove_univ this

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

Goal state before:
pp: α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
⊢ #↑A < #↑B

Tactic:
rcases finite_or_infinite B with hfin | hinf

Goal state after:
case inl
α : Type u
A B : Set α
hfin✝ : A.Finite
hlt : A ⊂ B
hfin : Finite ↑B
⊢ #↑A < #↑B

case inr
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite ↑B
⊢ #↑A < #↑B
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
⊢ (T \ S).Nonempty

Tactic:
rw [← mk_set_ne_zero_iff]
  intro h'
  exact h.not_ge ((le_mk_sdiff_add_mk T S).trans (by simp [h']))

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
x✝¹ : M →+ M₂
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm 0 • x✝) = 0 x✝

Tactic:
simp [DomMulAct.mk, MulOpposite.opEquiv]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
m : M
inst✝ : IsTorsionFree R M
hr : IsRegular r
⊢ r • m = 0 ↔ r • m = r • 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
m : M
inst✝ : IsTorsionFree R M
hr : IsRegular r
⊢ r • m = 0 ↔ r • m = 0
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, a • c) = (0, a • c)

Tactic:
smul_zero

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 : β
⊢ (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, a • 0) = (a • b, 0)

Tactic:
smul_zero

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, 0) = (a • b, 0)
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
⊢ mn.1 • 0 = 0

Tactic:
smul_zero

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
⊢ 0 = 0
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑(f' ^ (n + 1))

Tactic:
by
    rw [iterate_succ]
    exact (iterate_injective h n).comp 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
m : ↥N
⊢ (N.subtype ∘ₗ g ^ k) m = 0

Tactic:
rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]

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₂
S : Submodule R M
⊢ Injective ⇑(f.domRestrict S) ↔ Disjoint S f.ker

Tactic:
by
  simp [← ker_eq_bot, ker_domRestrict, disjoint_iff_comap_eq_bot]

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✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ comap f q ≤ comap (c • f) q

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

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ ∀ ⦃x : M⦄, f x ∈ q → c • f x ∈ q
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

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

Tactic:
induction n <;> simp [zero_mem, add_mem, one_mem, *]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -x✝ ∈ s.carrier

Tactic:
rw [← neg_one_mul]

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -1 * x✝ ∈ s.carrier
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ x✝ • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ 0 = 0
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
_hx : x✝ ∈ closure s
_hy : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
| mul _ _ _hx _hy hx hy =>

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A
inst✝³ : Algebra R✝ A
inst✝² : FaithfulSMul R✝ A
R : Type u_3
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ FaithfulSMul ℤ R

Tactic:
simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℤ R).injective_int

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

Goal state before:
pp: case mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
_hx : x✝ ∈ closure s
_hy : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
| mul _ _ _hx _hy hx hy =>

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
let U : Subring R :=
    Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
      (Submonoid.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)

Goal state after:
R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hp : DvdNotUnit p q
⊢ ¬IsUnit q

Tactic:
obtain ⟨-, x, hx, rfl⟩ := hp

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p x : M
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Irreducible (Associates.mk a) ↔ Irreducible a

Tactic:
by
  simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := a)]
  apply Iff.rfl.and
  constructor
  · rintro h x y rfl
    exact h _ _ <| .refl _
  · rintro h x y ⟨u, rfl⟩
    simpa using h (mul_assoc _ _ _)

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

Tactic:
refine Submodule.mem_map.trans ⟨?_, ?_⟩ <;> simp_rw [Submodule.mem_comap]
  · rintro ⟨⟨y, yO⟩, yN : y ∈ N, h⟩
    exact ⟨y, yO, yN, h⟩
  · rintro ⟨y, yO, yN, h⟩
    exact ⟨⟨y, yO⟩, yN, h⟩

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

Goal state before:
pp: case of_mem_closure
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)
⊢ x ∈ (span R s).toAddSubmonoid

Tactic:
case of_mem_closure =>
    refine closure_le.2 ?_ hx
    rintro - ⟨r, -, x, hx, rfl⟩
    exact smul_mem _ _ (subset_span hx)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x y : α
hdisjoint : Disjoint x y
x✝ : ↑(Iic (x ⊔ y))
hx : x ∈ Iic (x ⊔ y)
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = x ⊔ y

Tactic:
exact ⟨⟨y, le_sup_right⟩, hdisjoint, rfl⟩

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
p p' : Submodule R M
m : M
⊢ m ∈ p ⊔ p' ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
rw [mem_sup]

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
m : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
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
p p' : Submodule R M
⊢ p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
rw [eq_top_iff']
  refine forall_congr' fun m ↦ ?_
  rw [mem_sup]
  tauto

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

Goal state before:
pp: case refine_1
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✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

Tactic:
refine ⟨{x}, ?_, ?_⟩

Goal state after:
case refine_1.refine_1
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✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ↑{x} ⊆ S

case refine_1.refine_2
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✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ a • y + z + -a • y ∈ span R s

Tactic:
simp [hz, add_assoc]

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

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

Tactic:
intro hk s hsup

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
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ k • x ∈ restrictScalars R (span S t)

Tactic:
exact (span S t).smul_mem k (span_le_restrictScalars R S t 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 : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) = span R s

Tactic:
by
  apply le_antisymm
  · apply span_smul_le
  · convert! span_smul_le (r • s) ((hr.unit⁻¹ :) : R)
    simp [smul_smul]

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

Goal state before:
pp: case refine_4.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • 0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
smul_zero

Goal state after:
case refine_4.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ 0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
s' : Multiset M₀
hs' : s = 0 ::ₘ s'
⊢ s.prod = 0

Tactic:
simp [hs', Multiset.prod_cons]

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

Goal state before:
pp: case inr
α : 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
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x ∧ x ≤ c

Tactic:
exact ha.symm

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ (single a b₁) a = (single a b₂) a

Tactic:
rw [eq]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v ↦ if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
dsimp [Finsupp.prod]
  rw [f.support.prod_ite_eq']

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
this : ∀ (y : M), f y = 0
⊢ 0 = (↑n)⁻¹ • 0

Tactic:
smul_zero

Goal state after:
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
this : ∀ (y : M), f y = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
⊢ f x • 0 = 0

Tactic:
smul_zero

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ ∃ x, 1 < v x

pp: case inr
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : 1 < v x
⊢ ∃ x, 1 < v x

Tactic:
· refine ⟨x⁻¹, ?_⟩
    rw [map_inv₀]
    exact (one_lt_inv₀ <| v.pos hx₀).mpr h

Goal state after:
case inr
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : 1 < v x
⊢ ∃ x, 1 < v x
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
m : Multiset α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f m.prod ≤ (map f m).sum

Tactic:
induction m using Quotient.inductionOn with
  | h l => simp [l.apply_prod_le_sum_map _ h_one h_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (mapDomain f s).prod h = s.prod fun a b ↦ h (f a) b

Tactic:
by
  rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)

Tactic:
rw [eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a * 1 ≤ f a * (map f s').prod

Tactic:
by
      gcongr
      · exact le_trans (zero_le_one' β) (h1 a)
      · simp_all [one_le_prod]

Goal state after: