-- Mathlib/Data/Matroid/Sum.lean
lemma Finitary.sigma (h : ∀ i, (M i).Finitary) : (Matroid.sigma M).Finitary

Proof state:
case h.e'_3
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ J = Sigma.mk i ⁻¹' (Sigma.mk i '' J)

Tactic:
rw [sigma_mk_preimage_image_eq_self]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ Sigma.mk i '' J ⊆ I

Tactic:
simpa

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ (M i).Indep J

Tactic:
convert hI (Sigma.mk i '' J) (by simpa) (hJ.image _) i

Result:
case h.e'_3
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ J = Sigma.mk i ⁻¹' (Sigma.mk i '' J)

Proof state:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
⊢ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)

Tactic:
intro i

Result:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ (M i).Indep (Sigma.mk i ⁻¹' I)

Proof state:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma M).Indep J
⊢ (Matroid.sigma M).Indep I

Tactic:
simp only [sigma_indep_iff] at hI ⊢

Result:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
⊢ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)

Proof state:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sigma M).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩

Result:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma M).Indep J
⊢ (Matroid.sigma M).Indep I

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ ∀ J ⊆ Sigma.mk i ⁻¹' I, J.Finite → (M i).Indep J

Tactic:
intro J hJI hJ

Result:
case h
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk i ⁻¹' I
hJ : J.Finite
⊢ (M i).Indep J

Proof state:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ (M i).Indep (Sigma.mk i ⁻¹' I)

Tactic:
apply indep_of_forall_finite_subset_indep

Result:
case h
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
i : ι
⊢ ∀ J ⊆ Sigma.mk i ⁻¹' I, J.Finite → (M i).Indep J