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

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
· push Not at h
    rcases h with ⟨i, hi, hq⟩
    exact prod_eq_zero hi (by simp [hq])

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

Goal state before:
pp: case empty
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
f : ι → G₀
h : ∏ i ∈ ∅, f i ≠ 0
⊢ mk0 (∏ i ∈ ∅, f i) h = ∏ i ∈ ∅.attach, mk0 (f ↑i) ⋯

pp: case cons
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
f : ι → G₀
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (h : ∏ i ∈ s✝, f i ≠ 0), mk0 (∏ i ∈ s✝, f i) h = ∏ i ∈ s✝.attach, mk0 (f ↑i) ⋯
h : ∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i ≠ 0
⊢ mk0 (∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i) h = ∏ i ∈ (Finset.cons a✝¹ s✝ h✝).attach, mk0 (f ↑i) ⋯

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
f : ι → G₀
h : ∏ i ∈ ∅, f i ≠ 0
⊢ mk0 (∏ i ∈ ∅, f i) h = ∏ i ∈ ∅.attach, mk0 (f ↑i) ⋯

case cons
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
f : ι → G₀
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (h : ∏ i ∈ s✝, f i ≠ 0), mk0 (∏ i ∈ s✝, f i) h = ∏ i ∈ s✝.attach, mk0 (f ↑i) ⋯
h : ∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i ≠ 0
⊢ mk0 (∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i) h = ∏ i ∈ (Finset.cons a✝¹ s✝ h✝).attach, mk0 (f ↑i) ⋯
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
⊢ sSup {a | IsCompactElement a} = sSup {c | IsCompactElement c ∧ c ≤ ⊤}

Tactic:
simp_rw [le_top, and_true]

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 ≠ ⊥}

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

Goal state after:
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 ≠ ⊥}

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 ≠ ⊥}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi

Goal state before:
pp: case hi
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, (fun i ↦ a i ⋯) ∈ Fintype.piFinset t

pp: case hj
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset t, (fun i x ↦ a i) ∈ univ.pi t

pp: case left_inv
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, (fun i x ↦ (fun i ↦ a i ⋯) i) = a

pp: case right_inv
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset t, (fun i ↦ (fun i x ↦ a i) i ⋯) = a

pp: case h
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, f a = f fun a_2 x ↦ (fun i ↦ a i ⋯) a_2

Tactic:
<;>

Goal state after:
case hi
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, (fun i ↦ a i ⋯) ∈ Fintype.piFinset t

case hj
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset t, (fun i x ↦ a i) ∈ univ.pi t

case left_inv
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, (fun i x ↦ (fun i ↦ a i ⋯) i) = a

case right_inv
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset t, (fun i ↦ (fun i x ↦ a i) i ⋯) = a

case h
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, f a = f fun a_2 x ↦ (fun i ↦ a i ⋯) a_2
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 ≠ ⊥}

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

Goal state after:
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 ≠ ⊥}

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 ≠ ⊥}
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case pos.a
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∈ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
⊢ (f i).indicator (g i) j = g i j

Tactic:
simp only [Set.mem_iInter] at hj

Goal state after:
case pos.a
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
i : ι
hi : i ∈ s
hj : ∀ i ∈ s, j ∈ f i
⊢ (f i).indicator (g i) j = g i j
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case e'_3
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f i x✝ = (∏ i ∈ v, f i) x✝

pp: case e'_4
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f' i x✝ = (∏ i ∈ v, f' i) x✝

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f i x✝ = (∏ i ∈ v, f i) x✝

case e'_4
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f' i x✝ = (∏ i ∈ v, f' i) x✝
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case nil
M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
⊢ (map Neg.neg []).prod = (-1) ^ [].length * [].prod

pp: case cons
M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
head✝ : M
tail✝ : List M
tail_ih✝ : (map Neg.neg tail✝).prod = (-1) ^ tail✝.length * tail✝.prod
⊢ (map Neg.neg (head✝ :: tail✝)).prod = (-1) ^ (head✝ :: tail✝).length * (head✝ :: tail✝).prod

Tactic:
<;>

Goal state after:
case nil
M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
⊢ (map Neg.neg []).prod = (-1) ^ [].length * [].prod

case cons
M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
head✝ : M
tail✝ : List M
tail_ih✝ : (map Neg.neg tail✝).prod = (-1) ^ tail✝.length * tail✝.prod
⊢ (map Neg.neg (head✝ :: tail✝)).prod = (-1) ^ (head✝ :: tail✝).length * (head✝ :: tail✝).prod
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
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 =
    (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).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.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
hcard0 : s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

pp: case neg
α : 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
hcard0 : ¬s.card = 0
⊢ s.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
hcard0 : s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

case neg
α : 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
hcard0 : ¬s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons.e'_5.a.e'_4
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).2 = (Prod.map id (cons a) a✝²).2 + x✝.2

pp: case cons.e'_6.a.e'_3
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).1 = (Prod.map (cons a) id a✝²).1 + x✝.1

Tactic:
<;>

Goal state after:
case cons.e'_5.a.e'_4
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).2 = (Prod.map id (cons a) a✝²).2 + x✝.2

case cons.e'_6.a.e'_3
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).1 = (Prod.map (cons a) id a✝²).1 + x✝.1
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:
← Subtype.coe_le_coe,

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: ι : 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:
← Subtype.coe_le_coe,

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
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
⊢ comap f (p ⊔ q) = comap f p ⊔ comap f q

Tactic:
by
  apply map_injective_of_injective hf
  rw [map_sup, map_comap_eq_self, map_comap_eq_self hp, map_comap_eq_self hq]
  simp [sup_le_iff, hp, hq]

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

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s \ {i}, g i = ∏ i ∈ s \ {i}, f i

pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s \ {i}, h i = ∏ i ∈ s \ {i}, f i

Tactic:
<;>

Goal state after:
case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s \ {i}, g i = ∏ i ∈ s \ {i}, f i

case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s \ {i}, h i = ∏ i ∈ s \ {i}, f i
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∀ x ∈ s \ {i}, g x = f x

pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∀ x ∈ s \ {i}, h x = f x

Tactic:
<;>

Goal state after:
case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∀ x ∈ s \ {i}, g x = f x

case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∀ x ∈ s \ {i}, h x = f x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

pp: case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

pp: case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

pp: case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

pp: case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

pp: case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

pp: case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

pp: case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

pp: case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
h : j = i
⊢ f j = f i

pp: case neg
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
h : ¬j = i
⊢ 1 = 1

Tactic:
<;>

Goal state after:
case pos
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
h : j = i
⊢ f j = f i

case neg
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
h : ¬j = i
⊢ 1 = 1