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

Goal state before:
pp: case cons.mp
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) →
    ∀ (a_2 : α) (h : a_2 ∈ a ::ₘ m), f a_2 h ∈ t a_2

pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ a_2, a_2 ∈ t a ∧ ∃ a_3, (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons m a a_2 a_3 = f

Tactic:
·

Goal state after:
case cons.mp
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) →
    ∀ (a_2 : α) (h : a_2 ∈ a ::ₘ m), f a_2 h ∈ t a_2
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ a_2, a_2 ∈ t a ∧ ∃ a_3, (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons m a a_2 a_3 = f

Tactic:
·

Goal state after:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ a_2, a_2 ∈ t a ∧ ∃ a_3, (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons m a a_2 a_3 = f
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)

pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
·

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
·

Goal state after:
case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

pp: case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite

pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)

pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
·

Goal state after:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case refine_1
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

pp: case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})

Tactic:
·

Goal state after:
case refine_1
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})

Tactic:
·

Goal state after:
case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = x • 1 * y • 1

Tactic:
rw [smul_one_mul, smul_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: case ofNat
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹

pp: case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Tactic:
·

Goal state after:
case ofNat
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Tactic:
·

Goal state after:
case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₁
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k ⊆ v i

pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
·

Goal state after:
case h₁
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k ⊆ v i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
·

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t ↦ s ×ˢ t) '' C)

Tactic:
simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
·

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ (x : α), x ∈ s → p x⁻¹

Tactic:
rw [← (Equiv.inv _).forall_congr_right]

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∀ (a : α), ((Equiv.inv α) a)⁻¹ ∈ s → p ((Equiv.inv α) a)) ↔ ∀ (x : α), x ∈ s → p x⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
·

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inl
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))

pp: case inr
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
·

Goal state after:
case inl
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inr
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
·

Goal state after:
case inr
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inl
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i

pp: case inr
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j

Tactic:
·

Goal state after:
case inl
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inr
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j

Tactic:
·

Goal state after:
case inr
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

pp: case refine_2
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v

Tactic:
·

Goal state after:
case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

pp: case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

pp: case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
·

Goal state after:
case mp.inl
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
·

Goal state after:
case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_2
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v

Tactic:
·

Goal state after:
case refine_2
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
·

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
·

Goal state after:
case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1