mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single i m)
val✝ : Fintype ι
⊢ p (∑ i, Pi.single i (f i))

Tactic:
]

Goal state after:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single i m)
val✝ : Fintype ι
⊢ p (∑ i, Pi.single i (f i))
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ p (∏ i, Pi.mulSingle i (f i))

Tactic:
]

Goal state after:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ p (∏ i, Pi.mulSingle i (f i))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_4.refine_3
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))
x y : M
hx✝ : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy✝ : y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hx : r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy : r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • x + r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
]

Goal state after:
case refine_4.refine_3
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))
x y : M
hx✝ : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy✝ : y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hx : r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy : r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • x + r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case cons
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)

Tactic:
]

Goal state after:
case cons
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)
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
ι : Sort u_8
p : ι → Submodule R M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, (p i).toAddSubmonoid
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
]

Goal state after:
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
motive : M → Prop
x : M
hx : x ∈ ⨆ i, (p i).toAddSubmonoid
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
x✝ : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ (x₁, x₂) = (x₁, x₂)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ ?m.66 ~
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)

pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    ?m.66

pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length

Tactic:
]

Goal state after:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)

α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0

Tactic:
]

Goal state after:
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ 0 = a ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
]

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep fun k ↦ ⨅ i, f i (k i)
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
x : M
⊢ ∀ (s : Set (Submodule R M)), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ∀ (s : Set (Submodule R M)), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case cons
R : Type u_5
inst✝ : NonUnitalSemiring R
a x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ x + l.sum

Tactic:
]

Goal state after:
case cons
R : Type u_5
inst✝ : NonUnitalSemiring R
a x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ x + l.sum
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 (⨆ x ∈ ↑S, R ∙ x)

Tactic:
]

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.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 (S.sup fun x ↦ R ∙ x)

Tactic:
]

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 (S.sup fun x ↦ R ∙ x)
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : 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))

Tactic:
]

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
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
s : Submodule R M
⊢ s = s

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ ↑l

Tactic:
]

Goal state after:
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ ↑l
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalSemiring R
s✝ : Multiset R
a x : R
s : Multiset R
ih : (∀ (x : R), x ∈ s → a ∣ x) → a ∣ s.sum
h : ∀ (x_1 : R), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ x + s.sum

Tactic:
]

Goal state after:
R : Type u_4
inst✝ : NonUnitalSemiring R
s✝ : Multiset R
a x : R
s : Multiset R
ih : (∀ (x : R), x ∈ s → a ∣ x) → a ∣ s.sum
h : ∀ (x_1 : R), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ x + s.sum
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ((Finset.image (fun x ↦ x i) s).biUnion fun a ↦ {c ∈ s | c i = a}).SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
]

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ((Finset.image (fun x ↦ x i) s).biUnion fun a ↦ {c ∈ s | c i = a}).SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ (a ::ₘ (s - x), x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset

Tactic:
]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ (a ::ₘ (s - x), x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a a✝.sum

Tactic:
]

Goal state after:
case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a a✝.sum
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons.e_a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
x : Multiset α
hx : x ∈ s.powerset
⊢ (a ::ₘ (s - x), x) = (a ::ₘ (s - x), x)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
this : s.antidiagonal.card = 2 ^ s.card
⊢ s.antidiagonal.card = 2 ^ s.card

Tactic:
]

Goal state after:
α : Type u_1
s : Multiset α
this : s.antidiagonal.card = 2 ^ s.card
⊢ s.antidiagonal.card = 2 ^ s.card
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ ∀ a ∈ {c | IsCompactElement c ∧ c ≤ b}, a = ⊥

Tactic:
]

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ ∀ a ∈ {c | IsCompactElement c ∧ c ≤ b}, a = ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
]

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg.inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
a : { x // x ∈ Iic c }
ha : IsAtom a
hac : ↑a ≤ ↑⟨c, ⋯⟩
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
]

Goal state after:
case neg.inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
a : { x // x ∈ Iic c }
ha : IsAtom a
hac : ↑a ≤ ↑⟨c, ⋯⟩
⊢ ∃ a, IsAtom a ∧ a ≤ b
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
⊢ a ≤ ⊥

Tactic:
]

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: ι : 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 ≤ ↑⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩

Tactic:
]

Goal state after:
ι : 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 ≤ ↑⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩
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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ p i ≤ ⨆ i ∈ s, p i

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ p i ≤ ⨆ i ∈ s, p i
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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ sSup (comap N.subtype '' s) = ⊤

Tactic:
]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ sSup (comap N.subtype '' 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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
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✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hp : p ≤ f.range
⊢ p ≤ q ↔ p ≤ q

Tactic:
]

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
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1

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:
]

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
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1

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)
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 (sSup ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) c

Tactic:
]

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.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✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective ⇑f
hp : p ≤ f.range
hq : q ≤ f.range
⊢ p ⊔ q = p ⊔ q

pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective ⇑f
hp : p ≤ f.range
hq : q ≤ f.range
⊢ p ⊔ q ≤ f.range

Tactic:
]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective ⇑f
hp : p ≤ f.range
hq : q ≤ f.range
⊢ p ⊔ q ≤ f.range
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx✝ : y + z = x
hyzx : z = -y + x
⊢ z ∈ p

Tactic:
]

Goal state after:
case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx✝ : y + z = x
hyzx : z = -y + x
⊢ z ∈ p
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
⊢ ∀ b_1 ∈ {a | a ≤ c ∧ IsAtom a}, b_1 ≤ b ⊔ sSup s

Tactic:
]

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
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoidWithOne R
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ ↑(#({x ∈ s | p x})) = ↑(#({x ∈ s | p x}))

Tactic:
]

Goal state after: