internlm/Lean-Github huggingface dataset:
Theorem: ENat.tsum_subtype_eq_top_iff
Proof state before:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
his : i ∈ s
hi : ⟨i, his⟩ ∈ support fun a => f ↑a
⊢ ∃ a, (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) a = ⟨⟨i, his⟩, hi⟩
Tactic:
use ⟨i, ⟨his, hi⟩⟩
Proof state after:
no goals
Theorem: ENat.tsum_subtype_const_eq_top_of_ne_zero
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hs : s.Infinite
c : ℕ∞
hc : c ≠ 0
⊢ (s ∩ support fun x => c).Infinite
Tactic:
rwa [support_const hc, inter_univ]
Proof state after:
no goals
Theorem: ENat.tsum_le_tsum_comp_of_surjective
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g✝ : α → ℕ∞
f : α → β
hf : Surjective f
g : β → ℕ∞
⊢ ∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))
Tactic:
simp only [surjInv_eq hf]
Proof state after:
no goals
Theorem: ENat.tsum_comp_eq_tsum_of_equiv
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g✝ : α → ℕ∞
e : α ≃ β
g : β → ℕ∞
⊢ ∑' (x : α), g (e x) = ∑' (y : β), g y
Tactic:
rw [ENat.tsum_comp_eq_tsum_of_bijective e.bijective]
Proof state after:
no goals
Theorem: ENat.tsum_biUnion_le_tsum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g f : α → ℕ∞
s : Set ι
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑' (x : ↑(⋃ i, t ↑i)), f ↑x
Tactic:
rw [tsum_congr_subtype]
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g f : α → ℕ∞
s : Set ι
t : ι → Set α
⊢ ∀ (x : α), x ∈ ⋃ i ∈ s, t i ↔ x ∈ ⋃ i, t ↑i
Theorem: ENat.tsum_biUnion_le_tsum
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g f : α → ℕ∞
s : Set ι
t : ι → Set α
⊢ ∀ (x : α), x ∈ ⋃ i ∈ s, t i ↔ x ∈ ⋃ i, t ↑i
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.tsum_iUnion_le
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x
Tactic:
rw [← tsum_fintype]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
Theorem: ENat.tsum_iUnion_le
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
Tactic:
exact ENat.tsum_iUnion_le_tsum f t
Proof state after:
no goals
Theorem: ENat.tsum_one'
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
obtain (hfin | hinf) := s.finite_or_infinite
Proof state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Theorem: ENat.tsum_one'
Proof state before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
rw [hinf.encard_eq, ENat.tsum_subtype_eq_top_of_inter_support_infinite]
Proof state after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ (s ∩ support 1).Infinite
Theorem: ENat.tsum_one'
Proof state before:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hinf : s.Infinite
⊢ (s ∩ support 1).Infinite
Tactic:
simpa
Proof state after:
no goals
Theorem: ENat.tsum_one'
Proof state before:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
have := hfin.fintype
Proof state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Theorem: ENat.tsum_one'
Proof state before:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ ∑' (i : ↑s), 1 ↑i = s.encard
Tactic:
convert tsum_eq_sum (β := s) (f := (1 : s → ℕ∞)) (s := Finset.univ) (by simp)
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ s.encard = ∑ b : ↑s, 1 b
Theorem: ENat.tsum_one'
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ s.encard = ∑ b : ↑s, 1 b
Tactic:
simp only [Pi.one_apply, Finset.sum_const, nsmul_eq_mul, mul_one,
  encard_eq_coe_toFinset_card, toFinset_card, Nat.cast_inj]
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ Fintype.card ↑s = Finset.univ.card
Theorem: ENat.tsum_one'
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ Fintype.card ↑s = Finset.univ.card
Tactic:
rfl
Proof state after:
no goals
Theorem: ENat.tsum_one'
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
hfin : s.Finite
this : Fintype ↑s
⊢ ∀ b ∉ Finset.univ, 1 b = 0
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.tsum_subtype_const
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
c : ℕ∞
⊢ ∑' (x : ↑s), c = c * s.encard
Tactic:
rw [← ENat.tsum_one s, ENat.mul_tsum, mul_one]
Proof state after:
no goals
Theorem: ENat.tsum_const
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : ℕ∞
⊢ ∑' (x : ι), c = c * univ.encard
Tactic:
rw [← tsum_univ, ENat.tsum_subtype_const]
Proof state after:
no goals
Theorem: ENat.encard_support_le_tsum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
⊢ (support f).encard ≤ ∑' (x : α), f x
Tactic:
rw [← ENat.tsum_one', tsum_subtype]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
⊢ ∑' (x : α), (support f).indicator 1 x ≤ ∑' (x : α), f x
Theorem: ENat.encard_support_le_tsum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
⊢ ∑' (x : α), (support f).indicator 1 x ≤ ∑' (x : α), f x
Tactic:
exact ENat.tsum_le_tsum <| ENat.indicator_support_le _
Proof state after:
no goals
Theorem: ENat.tsum_encard_eq_encard_iUnion
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
hI : univ.PairwiseDisjoint s
⊢ ∑' (i : ι), (s i).encard = (⋃ i, s i).encard
Tactic:
simp_rw [← ENat.tsum_one', ENat.tsum_iUnion_eq_tsum _ _ hI]
Proof state after:
no goals
Theorem: ENat.encard_iUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
⊢ (⋃ i, s i).encard ≤ ∑' (i : ι), (s i).encard
Tactic:
rw [← ENat.tsum_one]
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
⊢ ∑' (x : ↑(⋃ i, s i)), 1 ≤ ∑' (i : ι), (s i).encard
Theorem: ENat.encard_iUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
⊢ ∑' (x : ↑(⋃ i, s i)), 1 ≤ ∑' (i : ι), (s i).encard
Tactic:
exact (ENat.tsum_iUnion_le_tsum 1 s).trans_eq (by simp)
Proof state after:
no goals
Theorem: ENat.encard_iUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
⊢ ∑' (i : ι) (x : ↑(s i)), 1 ↑x = ∑' (i : ι), (s i).encard
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.tsum_encard_eq_encard_biUnion
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
⊢ ∑' (i : ↑t), (s ↑i).encard = (⋃ i ∈ t, s i).encard
Tactic:
rw [biUnion_eq_iUnion, ← ENat.tsum_encard_eq_encard_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
⊢ univ.PairwiseDisjoint fun x => s ↑x
Theorem: ENat.tsum_encard_eq_encard_biUnion
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
⊢ univ.PairwiseDisjoint fun x => s ↑x
Tactic:
rintro ⟨i,hi⟩ - ⟨j,hj⟩ - hij
Proof state after:
case mk.mk
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (Disjoint on fun x => s ↑x) ⟨i, hi⟩ ⟨j, hj⟩
Theorem: ENat.tsum_encard_eq_encard_biUnion
Proof state before:
case mk.mk
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (Disjoint on fun x => s ↑x) ⟨i, hi⟩ ⟨j, hj⟩
Tactic:
exact hI hi hj (by simpa using hij)
Proof state after:
no goals
Theorem: ENat.tsum_encard_eq_encard_biUnion
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ i ≠ ↑⟨j, hj⟩
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: ENat.encard_biUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
I : Set ι
⊢ (⋃ i ∈ I, s i).encard ≤ ∑' (i : ↑I), (s ↑i).encard
Tactic:
rw [biUnion_eq_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
I : Set ι
⊢ (⋃ x, s ↑x).encard ≤ ∑' (i : ↑I), (s ↑i).encard
Theorem: ENat.encard_biUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
I : Set ι
⊢ (⋃ x, s ↑x).encard ≤ ∑' (i : ↑I), (s ↑i).encard
Tactic:
apply encard_iUnion_le_tsum_encard
Proof state after:
no goals
Theorem: ENat.tsum_encard_eq_encard_sUnion
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
hc : c.PairwiseDisjoint id
⊢ ∑' (t : ↑c), (↑t).encard = (⋃₀ c).encard
Tactic:
rw [sUnion_eq_iUnion, ← ENat.tsum_encard_eq_encard_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
hc : c.PairwiseDisjoint id
⊢ univ.PairwiseDisjoint fun i => ↑i
Theorem: ENat.tsum_encard_eq_encard_sUnion
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
hc : c.PairwiseDisjoint id
⊢ univ.PairwiseDisjoint fun i => ↑i
Tactic:
rintro ⟨i,hi⟩ - ⟨j,hj⟩ - hij
Proof state after:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
hc : c.PairwiseDisjoint id
i : Set α
hi : i ∈ c
j : Set α
hj : j ∈ c
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (Disjoint on fun i => ↑i) ⟨i, hi⟩ ⟨j, hj⟩
Theorem: ENat.tsum_encard_eq_encard_sUnion
Proof state before:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
hc : c.PairwiseDisjoint id
i : Set α
hi : i ∈ c
j : Set α
hj : j ∈ c
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (Disjoint on fun i => ↑i) ⟨i, hi⟩ ⟨j, hj⟩
Tactic:
exact hc hi hj (by simpa using hij)
Proof state after:
no goals
Theorem: ENat.tsum_encard_eq_encard_sUnion
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
hc : c.PairwiseDisjoint id
i : Set α
hi : i ∈ c
j : Set α
hj : j ∈ c
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ i ≠ ↑⟨j, hj⟩
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: ENat.encard_sUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
⊢ (⋃₀ c).encard ≤ ∑' (s : ↑c), (↑s).encard
Tactic:
rw [sUnion_eq_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
⊢ (⋃ i, ↑i).encard ≤ ∑' (s : ↑c), (↑s).encard
Theorem: ENat.encard_sUnion_le_tsum_encard
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : Set (Set α)
⊢ (⋃ i, ↑i).encard ≤ ∑' (s : ↑c), (↑s).encard
Tactic:
apply encard_iUnion_le_tsum_encard
Proof state after:
no goals
Theorem: ENat.tsum_inter_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ ∑' (a : α), (s ∩ f ⁻¹' {a}).encard = s.encard
Tactic:
rw [ENat.tsum_encard_eq_encard_iUnion]
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ (⋃ i, s ∩ f ⁻¹' {i}).encard = s.encard

α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ univ.PairwiseDisjoint fun a => s ∩ f ⁻¹' {a}
Theorem: ENat.tsum_inter_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ univ.PairwiseDisjoint fun a => s ∩ f ⁻¹' {a}
Tactic:
refine fun i _ j _ hij ↦ disjoint_iff_forall_ne.2 ?_
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
i : α
x✝¹ : i ∈ univ
j : α
x✝ : j ∈ univ
hij : i ≠ j
⊢ ∀ ⦃a : ι⦄, a ∈ (fun a => s ∩ f ⁻¹' {a}) i → ∀ ⦃b : ι⦄, b ∈ (fun a => s ∩ f ⁻¹' {a}) j → a ≠ b
Theorem: ENat.tsum_inter_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
i : α
x✝¹ : i ∈ univ
j : α
x✝ : j ∈ univ
hij : i ≠ j
⊢ ∀ ⦃a : ι⦄, a ∈ (fun a => s ∩ f ⁻¹' {a}) i → ∀ ⦃b : ι⦄, b ∈ (fun a => s ∩ f ⁻¹' {a}) j → a ≠ b
Tactic:
rintro a ⟨-,rfl⟩ _ ⟨-,rfl⟩ rfl
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
a : ι
x✝¹ x✝ : f a ∈ univ
hij : f a ≠ f a
⊢ False
Theorem: ENat.tsum_inter_fiber_eq
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
a : ι
x✝¹ x✝ : f a ∈ univ
hij : f a ≠ f a
⊢ False
Tactic:
exact hij rfl
Proof state after:
no goals
Theorem: ENat.tsum_inter_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ (⋃ i, s ∩ f ⁻¹' {i}).encard = s.encard
Tactic:
congr
Proof state after:
case e_s
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ ⋃ i, s ∩ f ⁻¹' {i} = s
Theorem: ENat.tsum_inter_fiber_eq
Proof state before:
case e_s
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
s : Set ι
f : ι → α
⊢ ⋃ i, s ∩ f ⁻¹' {i} = s
Tactic:
aesop
Proof state after:
no goals
Theorem: ENat.tsum_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
f : ι → α
⊢ ∑' (a : α), (f ⁻¹' {a}).encard = univ.encard
Tactic:
rw [← ENat.tsum_inter_fiber_eq (s := univ) f, tsum_congr]
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
f : ι → α
⊢ ∀ (b : α), (f ⁻¹' {b}).encard = (univ ∩ f ⁻¹' {b}).encard
Theorem: ENat.tsum_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
f : ι → α
⊢ ∀ (b : α), (f ⁻¹' {b}).encard = (univ ∩ f ⁻¹' {b}).encard
Tactic:
intro b
Proof state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
f : ι → α
b : α
⊢ (f ⁻¹' {b}).encard = (univ ∩ f ⁻¹' {b}).encard
Theorem: ENat.tsum_fiber_eq
Proof state before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
ι : Type u_4
f : ι → α
b : α
⊢ (f ⁻¹' {b}).encard = (univ ∩ f ⁻¹' {b}).encard
Tactic:
rw [univ_inter]
Proof state after:
no goals
Theorem: Matroid.Iso.dep_image_iff
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
D : Set ↑M.E
⊢ M.Dep ↑D ↔ N.Dep ↑(⇑e '' D)
Tactic:
rw [← not_indep_iff, e.indep_image_iff, not_indep_iff]
Proof state after:
no goals
Theorem: Matroid.Iso.preimage_image
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑M.E
⊢ ⇑e ⁻¹' (⇑e '' X) = X
Tactic:
rw [← e.image_symm_eq_preimage, e.symm_image_image]
Proof state after:
no goals
Theorem: Matroid.Iso.image_preimage
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑N.E
⊢ ⇑e '' (⇑e ⁻¹' X) = X
Tactic:
rw [← e.image_symm_eq_preimage, e.image_symm_image]
Proof state after:
no goals
Theorem: Matroid.Iso.preimage_subset_iff
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑N.E
Y : Set ↑M.E
⊢ ⇑e ⁻¹' X ⊆ Y ↔ X ⊆ ⇑e '' Y
Tactic:
rw [← e.image_symm_eq_preimage, image_subset_iff, e.preimage_symm_eq_image]
Proof state after:
no goals
Theorem: Matroid.Iso.base_image
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ N.Base ↑(⇑e '' B)
Tactic:
rw [base_iff_maximal_indep, ← e.indep_image_iff, and_iff_right hB.indep]
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ ∀ (I : Set β), N.Indep I → ↑(⇑e '' B) ⊆ I → ↑(⇑e '' B) = I
Theorem: Matroid.Iso.base_image
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ ∀ (I : Set β), N.Indep I → ↑(⇑e '' B) ⊆ I → ↑(⇑e '' B) = I
Tactic:
intro I hI h'
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set β
hI : N.Indep I
h' : ↑(⇑e '' B) ⊆ I
⊢ ↑(⇑e '' B) = I
Theorem: Matroid.Iso.base_image
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set β
hI : N.Indep I
h' : ↑(⇑e '' B) ⊆ I
⊢ ↑(⇑e '' B) = I
Tactic:
obtain ⟨I, rfl⟩ := Subset.eq_image_val hI.subset_ground
Proof state after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
⊢ ↑(⇑e '' B) = ↑I
Theorem: Matroid.Iso.base_image
Proof state before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
⊢ ↑(⇑e '' B) = ↑I
Tactic:
replace hB := hB.eq_of_subset_indep (e.symm.image_indep hI)
Proof state after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : ↑B ⊆ ↑(⇑e.symm '' I) → ↑B = ↑(⇑e.symm '' I)
⊢ ↑(⇑e '' B) = ↑I
Theorem: Matroid.Iso.base_image
Proof state before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : ↑B ⊆ ↑(⇑e.symm '' I) → ↑B = ↑(⇑e.symm '' I)
⊢ ↑(⇑e '' B) = ↑I
Tactic:
simp only [image_subset_iff, preimage_val_image_val_eq_self, image_val_inj,
  image_symm_eq_preimage] at hB
Proof state after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I
Theorem: Matroid.Iso.base_image
Proof state before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I
Tactic:
simp only [image_subset_iff, preimage_val_image_val_eq_self] at h'
Proof state after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
h' : B ⊆ ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I
Theorem: Matroid.Iso.base_image
Proof state before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
h' : B ⊆ ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I
Tactic:
simp [hB h', image_image]
Proof state after:
no goals
Theorem: Matroid.Iso.base_image_iff
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
h : N.Base ↑(⇑e '' B)
⊢ M.Base ↑B
Tactic:
simpa using e.symm.base_image h
Proof state after:
no goals
Theorem: Matroid.Iso.nonempty_right
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : M.Nonempty
⊢ N.Nonempty
Tactic:
obtain ⟨x,hx⟩ := M.ground_nonempty
Proof state after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : M.Nonempty
x : α
hx : x ∈ M.E
⊢ N.Nonempty
Theorem: Matroid.Iso.nonempty_right
Proof state before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : M.Nonempty
x : α
hx : x ∈ M.E
⊢ N.Nonempty
Tactic:
exact ⟨e ⟨x,hx⟩, Subtype.coe_prop (e ⟨x, hx⟩)⟩
Proof state after:
no goals
Theorem: Matroid.Iso.right_eq_empty
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
⊢ N = emptyOn β
Tactic:
rw [← ground_eq_empty_iff]
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
⊢ N.E = ∅
Theorem: Matroid.Iso.right_eq_empty
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
⊢ N.E = ∅
Tactic:
have h := e.toEquiv
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑(emptyOn α).E ≃ ↑N.E
⊢ N.E = ∅
Theorem: Matroid.Iso.right_eq_empty
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑(emptyOn α).E ≃ ↑N.E
⊢ N.E = ∅
Tactic:
simp only [emptyOn_ground] at h
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑∅ ≃ ↑N.E
⊢ N.E = ∅
Theorem: Matroid.Iso.right_eq_empty
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑∅ ≃ ↑N.E
⊢ N.E = ∅
Tactic:
exact isEmpty_coe_sort.mp h.symm.isEmpty
Proof state after:
no goals
Theorem: Matroid.Iso.basis_image_iff
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Basis ↑I ↑X ↔ N.Basis ↑(⇑e '' I) ↑(⇑e '' X)
Tactic:
simp only [image_subset_iff, Subtype.coe_preimage_self, subset_univ, basis_iff_mem_maximals,
  mem_maximals_iff, mem_setOf_eq, ← e.indep_image_iff, preimage_val_image_val_eq_self, and_imp,
  preimage_image, and_congr_right_iff]
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Indep ↑I →
    I ⊆ X →
      ((∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
        ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y)
Theorem: Matroid.Iso.basis_image_iff
Proof state before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Indep ↑I →
    I ⊆ X →
      ((∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
        ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y)
Tactic:
intro hI hIX
Proof state after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
    ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y