[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
f : σ → A
i : σ
⊢ (1 •
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    f i
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
have : C (σ := σ) a • D f = D (C a * f) := by simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ ↑C a • ↑D f = ↑D (↑C a * f)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : ↑C a • ↑D f = ↑D (↑C a * f)
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
rw [this, C_mul', D.map_smul]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
⊢ (∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p) ↔
    ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
[PROOFSTEP]
refine' ⟨fun H p i => H _ _, fun H => _⟩
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
⊢ ∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
⊢ ∀ (r : R), ↑D (↑C r) = 0
[PROOFSTEP]
intro r
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
r : R
⊢ ↑D (↑C r) = 0
[PROOFSTEP]
rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
⊢ ∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
have : ∀ p i, D (p * X i) = p • D (X i) + (X i : MvPolynomial σ R) • D p :=
  by
  intro p i
  induction' p using MvPolynomial.induction_on' with s r p q hp hq
  ·
    rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc, smul_add, D.map_smul,
      smul_comm r (X i)]
  · rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
⊢ ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
[PROOFSTEP]
intro p i
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
p : MvPolynomial σ R
i : σ
⊢ ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
[PROOFSTEP]
induction' p using MvPolynomial.induction_on' with s r p q hp hq
[GOAL]
case h1
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
i : σ
s : σ →₀ ℕ
r : R
⊢ ↑D (↑(monomial s) r * X i) = ↑(monomial s) r • ↑D (X i) + X i • ↑D (↑(monomial s) r)
[PROOFSTEP]
rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc, smul_add, D.map_smul,
  smul_comm r (X i)]
[GOAL]
case h2
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
i : σ
p q : MvPolynomial σ R
hp : ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
hq : ↑D (q * X i) = q • ↑D (X i) + X i • ↑D q
⊢ ↑D ((p + q) * X i) = (p + q) • ↑D (X i) + X i • ↑D (p + q)
[PROOFSTEP]
rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
⊢ ∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
intro p q
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
⊢ ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
induction q using MvPolynomial.induction_on with
| h_C c => rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
| h_X q i hq =>
  simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
  rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
⊢ ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
induction q using MvPolynomial.induction_on with
| h_C c => rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
| h_X q i hq =>
  simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
  rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
case h_C
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p : MvPolynomial σ R
c : R
⊢ ↑D (p * ↑C c) = p • ↑D (↑C c) + ↑C c • ↑D p
[PROOFSTEP]

| h_C c => rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
[GOAL]
case h_C
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p : MvPolynomial σ R
c : R
⊢ ↑D (p * ↑C c) = p • ↑D (↑C c) + ↑C c • ↑D p
[PROOFSTEP]
rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ ↑D (p * (q₁ + q₂)) = p • ↑D (q₁ + q₂) + (q₁ + q₂) • ↑D p
[PROOFSTEP]

| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ ↑D (p * (q₁ + q₂)) = p • ↑D (q₁ + q₂) + (q₁ + q₂) • ↑D p
[PROOFSTEP]
simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ p • ↑D q₁ + q₁ • ↑D p + (p • ↑D q₂ + q₂ • ↑D p) = p • ↑D q₁ + p • ↑D q₂ + (q₁ • ↑D p + q₂ • ↑D p)
[PROOFSTEP]
abel
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ p • ↑D q₁ + q₁ • ↑D p + (p • ↑D q₂ + q₂ • ↑D p) = p • ↑D q₁ + p • ↑D q₂ + (q₁ • ↑D p + q₂ • ↑D p)
[PROOFSTEP]
abel
[GOAL]
case h_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
i : σ
hq : ↑D (p * q) = p • ↑D q + q • ↑D p
⊢ ↑D (p * (q * X i)) = p • ↑D (q * X i) + (q * X i) • ↑D p
[PROOFSTEP]

| h_X q i hq =>
  simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
  rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
case h_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
i : σ
hq : ↑D (p * q) = p • ↑D q + q • ↑D p
⊢ ↑D (p * (q * X i)) = p • ↑D (q * X i) + (q * X i) • ↑D p
[PROOFSTEP]
simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
[GOAL]
case h_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
i : σ
hq : ↑D (p * q) = p • ↑D q + q • ↑D p
⊢ p • q • ↑D (X i) + (X i • p • ↑D q + X i • q • ↑D p) = p • q • ↑D (X i) + (p • X i • ↑D q + q • X i • ↑D p)
[PROOFSTEP]
rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ↑(mkDerivationₗ R f) (↑(monomial s) 1 * X i) =
    ↑(monomial s) 1 • ↑(mkDerivationₗ R f) (X i) + X i • ↑(mkDerivationₗ R f) (↑(monomial s) 1)
[PROOFSTEP]
simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum (s + Finsupp.single i 1) fun i_1 k =>
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_add_index'] <;> [skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul])]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum (s + Finsupp.single i 1) fun i_1 k =>
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_add_index']
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
skip
[GOAL]
case h_zero
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ∀ (a : σ), ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑0 • f a = 0
[PROOFSTEP]
simp
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ∀ (a : σ) (b₁ b₂ : ℕ),
    ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑(b₁ + b₂) • f a =
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑b₁ • f a +
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑b₂ • f a
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i a✝ : σ
b₁✝ b₂✝ : ℕ
⊢ ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a✝ 1)) ↑(b₁✝ + b₂✝) • f a✝ =
    ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a✝ 1)) ↑b₁✝ • f a✝ +
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a✝ 1)) ↑b₂✝ • f a✝
[PROOFSTEP]
simp only [Nat.cast_add, (monomial _).map_add, add_smul]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_single_index, Finsupp.sum_single_index]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i =
    ↑(monomial s) 1 • ↑(monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
skip
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ↑(monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑0 • f i = 0
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑0 • f i = 0
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i =
    ↑(monomial s) 1 • ↑(monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm, Finsupp.smul_sum]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (↑(monomial s) 1 • f i +
      Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    ↑(monomial s) 1 • f i +
      Finsupp.sum s fun a b => ↑(monomial (Finsupp.single i 1)) 1 • ↑(monomial (s - Finsupp.single a 1)) ↑b • f a
[PROOFSTEP]
refine' congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => _)
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i j : σ
hj : j ∈ s.support
⊢ (fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) j (↑s j) =
    (fun a b => ↑(monomial (Finsupp.single i 1)) 1 • ↑(monomial (s - Finsupp.single a 1)) ↑b • f a) j (↑s j)
[PROOFSTEP]
dsimp only
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i j : σ
hj : j ∈ s.support
⊢ ↑(monomial (s + Finsupp.single i 1 - Finsupp.single j 1)) ↑(↑s j) • f j =
    ↑(monomial (Finsupp.single i 1)) 1 • ↑(monomial (s - Finsupp.single j 1)) ↑(↑s j) • f j
[PROOFSTEP]
rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]
[GOAL]
case h
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i j : σ
hj : j ∈ s.support
⊢ Finsupp.single j 1 ≤ s
[PROOFSTEP]
rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]


[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Finset.Nonempty (Finset.sigma s t) ↔ ∃ i, i ∈ s ∧ Finset.Nonempty (t i)
[PROOFSTEP]
simp [Finset.Nonempty]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Finset.sigma s t = ∅ ↔ ∀ (i : ι), i ∈ s → t i = ∅
[PROOFSTEP]
simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Set.PairwiseDisjoint ↑s fun i => map (Embedding.sigmaMk i) (t i)
[PROOFSTEP]
intro i _ j _ hij
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (_root_.Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j
[PROOFSTEP]
rw [Function.onFun, disjoint_left]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → ¬a ∈ map (Embedding.sigmaMk j) (t j)
[PROOFSTEP]
simp_rw [mem_map, Function.Embedding.sigmaMk_apply]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄,
    (∃ a_1, a_1 ∈ t i ∧ { fst := i, snd := a_1 } = a) → ¬∃ a_2, a_2 ∈ t j ∧ { fst := j, snd := a_2 } = a
[PROOFSTEP]
rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : { fst := j, snd := z } = { fst := i, snd := y }
⊢ False
[PROOFSTEP]
exact hij (congr_arg Sigma.fst hz'.symm)
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Finset.sigma s t = Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Finset.sigma s t ↔
    { fst := x, snd := y } ∈ Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
[PROOFSTEP]
simp [and_left_comm]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ sup (Finset.sigma s t) f = sup s fun i => sup (t i) fun b => f { fst := i, snd := b }
[PROOFSTEP]
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a),
      a ∈ s → b ∈ t a → f { fst := a, snd := b } ≤ sup s fun i => sup (t i) fun b => f { fst := i, snd := b }) ∧
    ∀ (b : ι), b ∈ s → ∀ (b_1 : α b), b_1 ∈ t b → f { fst := b, snd := b_1 } ≤ sup (Finset.sigma s t) f
[PROOFSTEP]
exact
  ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
    le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
⊢ x ∈ sigmaLift f a b ↔ ∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
obtain ⟨⟨i, a⟩, j, b⟩ := a, b
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := j, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
[PROOFSTEP]
obtain rfl | h := Decidable.eq_or_ne i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } →
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)
[PROOFSTEP]
simp_rw [sigmaLift]
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (x ∈ if h : True then map (Embedding.sigmaMk i) (f a b) else ∅) →
    ∃ h h_1, x.snd ∈ f ((_ : { fst := i, snd := a }.fst = x.fst) ▸ a) ((_ : { fst := i, snd := b }.fst = x.fst) ▸ b)
[PROOFSTEP]
simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index, and_imp]
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ ∀ (x_1 : γ i),
    x_1 ∈ f a b →
      { fst := i, snd := x_1 } = x →
        ∃ h h_1, x.snd ∈ f ((_ : { fst := i, snd := a }.fst = x.fst) ▸ a) ((_ : { fst := i, snd := b }.fst = x.fst) ▸ b)
[PROOFSTEP]
rintro x hx rfl
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx : x ∈ f a b
⊢ ∃ h h_1,
    { fst := i, snd := x }.snd ∈
      f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := x }.fst) ▸ a)
        ((_ : { fst := i, snd := b }.fst = { fst := i, snd := x }.fst) ▸ b)
[PROOFSTEP]
exact ⟨rfl, rfl, hx⟩
[GOAL]
case mk.mk.inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)) →
    x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b }
[PROOFSTEP]
rintro ⟨⟨⟩, ⟨⟩, hx⟩
[GOAL]
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ x ∈ sigmaLift f { fst := x.1, snd := a } { fst := x.1, snd := b }
[PROOFSTEP]
rw [sigmaLift, dif_pos rfl, mem_map]
[GOAL]
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ ∃ a_1,
    a_1 ∈
        f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
          { fst := x.1, snd := b }.snd ∧
      ↑(Embedding.sigmaMk { fst := x.1, snd := b }.fst) a_1 = x
[PROOFSTEP]
exact ⟨_, hx, by simp [Sigma.ext_iff]⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ ↑(Embedding.sigmaMk { fst := x.1, snd := b }.fst) x.snd = x
[PROOFSTEP]
simp [Sigma.ext_iff]
[GOAL]
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := j, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
[PROOFSTEP]
rw [sigmaLift, dif_neg h]
[GOAL]
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ ∅ ↔ ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
[PROOFSTEP]
refine' iff_of_false (not_mem_empty _) _
[GOAL]
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
[PROOFSTEP]
rintro ⟨⟨⟩, ⟨⟩, _⟩
[GOAL]
case mk.mk.inr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
h : x.1 ≠ x.1
h✝ :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ False
[PROOFSTEP]
exact h rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ { fst := i, snd := x } ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } ↔ x ∈ f a b
[PROOFSTEP]
rw [sigmaLift, dif_pos rfl, mem_map]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1,
      a_1 ∈
          f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
            { fst := i, snd := b }.snd ∧
        ↑(Embedding.sigmaMk { fst := i, snd := b }.fst) a_1 = { fst := i, snd := x }) ↔
    x ∈ f a b
[PROOFSTEP]
refine' ⟨_, fun hx => ⟨_, hx, rfl⟩⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1,
      a_1 ∈
          f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
            { fst := i, snd := b }.snd ∧
        ↑(Embedding.sigmaMk { fst := i, snd := b }.fst) a_1 = { fst := i, snd := x }) →
    x ∈ f a b
[PROOFSTEP]
rintro ⟨x, hx, _, rfl⟩
[GOAL]
case intro.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx :
  x ∈
    f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
      { fst := i, snd := b }.snd
⊢ x ∈ f a b
[PROOFSTEP]
exact hx
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬x ∈ sigmaLift f a b
[PROOFSTEP]
rw [mem_sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
exact fun H => h H.fst
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬x ∈ sigmaLift f a b
[PROOFSTEP]
rw [mem_sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
exact fun H => h H.snd.fst
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ Finset.Nonempty (sigmaLift f a b) ↔ ∃ h, Finset.Nonempty (f (h ▸ a.snd) b.snd)
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty, sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) ≠ ∅ ↔ ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ ≠ ∅ ↔ ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
simp_rw [sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) = ∅ ↔
    ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
simp [h, forall_prop_of_true h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
simp [h, forall_prop_of_false h]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ⊆ sigmaLift g a b
[PROOFSTEP]
rintro x hx
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b
[PROOFSTEP]
rw [mem_sigmaLift] at hx ⊢
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
hx : ∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ ha hb, x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
obtain ⟨ha, hb, hx⟩ := hx
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
ha : a.fst = x.fst
hb : b.fst = x.fst
hx : x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ ha hb, x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
exact ⟨ha, hb, h hx⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ card (sigmaLift f a b) = if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
[PROOFSTEP]
simp_rw [sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ card (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ card (map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd)) = card (f (h ▸ a.snd) b.snd)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ card ∅ = 0
[PROOFSTEP]
simp [h]


[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ (i : ι), f i) ↔ ∀ (i : ι), Sized r (f i)
[PROOFSTEP]
simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → card x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → card x = r
[PROOFSTEP]
exact forall_swap
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : (i : ι) → κ i → Set (Finset α)
⊢ Sized r (⋃ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Sized r (f i j)
[PROOFSTEP]
simp only [Set.sized_iUnion]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
A : Finset α
⊢ A ∈ 𝒜 → A ∈ powersetLen r univ ↔ A ∈ ↑𝒜 → card A = r
[PROOFSTEP]
rw [mem_powerset_len_univ_iff, mem_coe]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) r
[PROOFSTEP]
rw [Fintype.card, ← card_powersetLen]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ card (powersetLen r univ)
[PROOFSTEP]
exact card_le_of_subset (subset_powersetLen_univ_iff.mpr h𝒜)
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
[PROOFSTEP]
rw [← card_biUnion, biUnion_slice]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∀ (x : ℕ), x ∈ Iic (Fintype.card α) → ∀ (y : ℕ), y ∈ Iic (Fintype.card α) → x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)
[PROOFSTEP]
exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)


[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ InjOn f (f ⁻¹' ↑∅)
[PROOFSTEP]
simp [InjOn]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ ↑(preimage ∅ f (_ : ∀ (a : α), a ∈ f ⁻¹' ↑∅ → ∀ (a_2 : α), a_2 ∈ f ⁻¹' ↑∅ → f a = f a_2 → a = a_2)) = ↑∅
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype β
hf : InjOn f (f ⁻¹' ↑univ)
⊢ ↑(preimage univ f hf) = ↑univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' ↑s)
ht : InjOn f (f ⁻¹' ↑t)
⊢ ↑(preimage (s ∩ t) f
        (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑(s ∩ t) → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑(s ∩ t) → f x₁ = f x₂ → x₁ = x₂)) =
    ↑(preimage s f hs ∩ preimage t f ht)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hst : InjOn f (f ⁻¹' ↑(s ∪ t))
⊢ ↑(preimage (s ∪ t) f hst) =
    ↑(preimage s f (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑s → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑s → f x₁ = f x₂ → x₁ = x₂) ∪
        preimage t f (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑t → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑t → f x₁ = f x₂ → x₁ = x₂))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
s : Finset β
hf : Injective f
⊢ ↑(preimage sᶜ f (_ : InjOn f (f ⁻¹' ↑sᶜ))) = ↑(preimage s f (_ : InjOn f (f ⁻¹' ↑s)))ᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
hf : InjOn f (f ⁻¹' ↑t)
⊢ (∀ (x : α), x ∈ s → f x ∈ t) ↔ s ⊆ preimage t f hf
[PROOFSTEP]
simp only [subset_iff, mem_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ preimage t ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑t))
[PROOFSTEP]
classical rw [map_eq_image, image_subset_iff_subset_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ preimage t ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑t))
[PROOFSTEP]
rw [map_eq_image, image_subset_iff_subset_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(image f (preimage s f hf)) = ↑(filter (fun x => x ∈ Set.range f) s)
[PROOFSTEP]
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range, ← Set.sep_mem_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ ↑(image f (preimage s f (_ : InjOn f (f ⁻¹' ↑s)))) = ↑s
[PROOFSTEP]
simpa using hf.image_eq
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u x, s = map f u
[PROOFSTEP]
classical
refine' ⟨fun h => ⟨_, preimage_subset h, _⟩, _⟩
· rw [map_eq_image, image_preimage, filter_true_of_mem]
  exact fun x hx ↦ coe_map_subset_range _ _ (h hx)
· rintro ⟨u, hut, rfl⟩
  exact map_subset_map.2 hut
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u x, s = map f u
[PROOFSTEP]
refine' ⟨fun h => ⟨_, preimage_subset h, _⟩, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
h : s ⊆ map f t
⊢ s = map f (preimage s ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑s)))
[PROOFSTEP]
rw [map_eq_image, image_preimage, filter_true_of_mem]
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
h : s ⊆ map f t
⊢ ∀ (x : β), x ∈ s → x ∈ Set.range ↑f
[PROOFSTEP]
exact fun x hx ↦ coe_map_subset_range _ _ (h hx)
[GOAL]
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ (∃ u x, s = map f u) → s ⊆ map f t
[PROOFSTEP]
rintro ⟨u, hut, rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
t u : Finset α
hut : u ⊆ t
⊢ map f u ⊆ map f t
[PROOFSTEP]
exact map_subset_map.2 hut
[GOAL]
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
⊢ (Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) =
    filter (fun a => a.fst ∈ t) s
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ (x ∈ Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) ↔
    x ∈ filter (fun a => a.fst ∈ t) s
[PROOFSTEP]
simp [and_comm]
[GOAL]
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ (Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) = s
[PROOFSTEP]
rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
[PROOFSTEP]
haveI := Classical.decEq γ
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
[PROOFSTEP]
calc
  (∏ x in preimage s f hf, g (f x)) = ∏ x in image f (preimage s f hf), g x :=
    Eq.symm <| prod_image <| by simpa only [mem_preimage, InjOn] using hf
  _ = ∏ x in s.filter fun x => x ∈ Set.range f, g x := by rw [image_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∀ (x : α), x ∈ preimage s f hf → ∀ (y : α), y ∈ preimage s f hf → f x = f y → x = y
[PROOFSTEP]
simpa only [mem_preimage, InjOn] using hf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in image f (preimage s f hf), g x = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
[PROOFSTEP]
rw [image_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in s, g x
[PROOFSTEP]
classical
rw [prod_preimage', prod_filter_of_ne]
exact fun x hx => Not.imp_symm (hg x hx)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in s, g x
[PROOFSTEP]
rw [prod_preimage', prod_filter_of_ne]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∀ (x : γ), x ∈ s → g x ≠ 1 → x ∈ Set.range f
[PROOFSTEP]
exact fun x hx => Not.imp_symm (hg x hx)


[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.fst) (b mn.snd)
[PROOFSTEP]
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun mn => f (a mn.fst) (b mn.snd)) (i₁, i₂) (j₁, j₂)
[PROOFSTEP]
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun i => map A fun a => f a (b i)
[PROOFSTEP]
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => map A fun a => f a (b i)) (i₁, i₂) (j₁, j₂)
[PROOFSTEP]
simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b)
[PROOFSTEP]
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b) (i₁, i₂)
      (j₁, j₂)
[PROOFSTEP]
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁷ : Zero α
inst✝⁶ : Zero β
inst✝⁵ : Zero γ
inst✝⁴ : One α
inst✝³ : One β
inst✝² : One γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
hf₃ : f 1 1 = 1
⊢ (diagonal fun mn => f 1 1) = 1
[PROOFSTEP]
simp only [hf₃, diagonal_one]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N)
[PROOFSTEP]
ext ⟨i, i'⟩ ⟨j, j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) (i, i') (j, j') =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N) (i, i') (j, j')
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
⊢ ↑(↑(kroneckerMapBilinear f) (A * B)) (A' * B') = ↑(↑(kroneckerMapBilinear f) A) A' * ↑(↑(kroneckerMapBilinear f) B) B'
[PROOFSTEP]
ext ⟨i, i'⟩ ⟨j, j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑(kroneckerMapBilinear f) (A * B)) (A' * B') (i, i') (j, j') =
    (↑(↑(kroneckerMapBilinear f) A) A' * ↑(↑(kroneckerMapBilinear f) B) B') (i, i') (j, j')
[PROOFSTEP]
simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product,
  kroneckerMap_apply]
[GOAL]
case a.mk.h.mk
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑f (Finset.sum Finset.univ fun j_1 => A i j_1 * B j_1 j)) (Finset.sum Finset.univ fun j => A' i' j * B' j j') =
    Finset.sum Finset.univ fun x =>
      Finset.sum Finset.univ fun x_1 => ↑(↑f (A i x)) (A' i' x_1) * ↑(↑f (B x j)) (B' x_1 j')
[PROOFSTEP]
simp_rw [f.map_sum, LinearMap.sum_apply, LinearMap.map_sum, h_comm]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : AddCommMonoid γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
A : Matrix m m α
B : Matrix n n β
⊢ trace (↑(↑(kroneckerMapBilinear f) A) B) = ↑(↑f (trace A)) (trace B)
[PROOFSTEP]
simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂, map_sum, ←
  Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ det (↑(↑(kroneckerMapBilinear f) A) B) = det (↑(↑(kroneckerMapBilinear f) A) 1 * ↑(↑(kroneckerMapBilinear f) 1) B)
[PROOFSTEP]
rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ det (↑(↑(kroneckerMapBilinear f) A) 1 * ↑(↑(kroneckerMapBilinear f) 1) B) =
    det (blockDiagonal fun x => map A fun a => ↑(↑f a) 1) * det (blockDiagonal fun x => map B fun b => ↑(↑f 1) b)
[PROOFSTEP]
rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply, kroneckerMap_diagonal_right _ fun _ => _,
  kroneckerMapBilinear_apply_apply, kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : β), ↑(↑f 0) x = 0
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : β
⊢ ↑(↑f 0) x✝ = 0
[PROOFSTEP]
exact LinearMap.map_zero₂ _ _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : α), ↑(↑f x) 0 = 0
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : α
⊢ ↑(↑f x✝) 0 = 0
[PROOFSTEP]
exact map_zero _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing α
inst✝⁴ : CommRing β
inst✝³ : CommRing γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ det (blockDiagonal fun x => map A fun a => ↑(↑f a) 1) * det (blockDiagonal fun x => map B fun b => ↑(↑f 1) b) =
    det (map A fun a => ↑(↑f a) 1) ^ Fintype.card n * det (map B fun b => ↑(↑f 1) b) ^ Fintype.card m
[PROOFSTEP]
simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ det (kroneckerMap (fun x x_1 => x * x_1) A B) = det A ^ Fintype.card n * det B ^ Fintype.card m
[PROOFSTEP]
refine' (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ det (map A fun a => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) a) 1) ^ Fintype.card n *
      det (map B fun b => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) 1) b) ^ Fintype.card m =
    det A ^ Fintype.card n * det B ^ Fintype.card m
[PROOFSTEP]
congr 3
[GOAL]
case e_a.e_a.e_M
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (map A fun a => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) a) 1) = A
[PROOFSTEP]
ext i j
[GOAL]
case e_a.e_a.e_M.a.h
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
i j : m
⊢ map A (fun a => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) a) 1) i j = A i j
[PROOFSTEP]
exact mul_one _
[GOAL]
case e_a.e_a.e_M
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (map B fun b => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) 1) b) = B
[PROOFSTEP]
ext i j
[GOAL]
case e_a.e_a.e_M.a.h
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
i j : n
⊢ map B (fun b => ↑(↑(AlgHom.toLinearMap (Algebra.lmul ℕ R)) 1) b) i j = B i j
[PROOFSTEP]
exact one_mul _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
by_cases hA : IsUnit A.det
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case neg.inl
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : IsEmpty n
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
  refine' mt (fun hAB => _) hA
  rw [det_kronecker] at hAB
  exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
⊢ ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
[PROOFSTEP]
refine' mt (fun hAB => _) hA
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
hAB : IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ IsUnit (det A)
[PROOFSTEP]
rw [det_kronecker] at hAB
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
hAB : IsUnit (det A ^ Fintype.card n * det B ^ Fintype.card m)
⊢ IsUnit (det A)
[PROOFSTEP]
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit (det A)
h✝ : Nonempty n
hAB : ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
by_cases hB : IsUnit B.det
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
cases isEmpty_or_nonempty m
[GOAL]
case neg.inl
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : IsEmpty m
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
  refine' mt (fun hAB => _) hB
  rw [det_kronecker] at hAB
  exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
⊢ ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
[PROOFSTEP]
refine' mt (fun hAB => _) hB
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
hAB : IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ IsUnit (det B)
[PROOFSTEP]
rw [det_kronecker] at hAB
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
hAB : IsUnit (det A ^ Fintype.card n * det B ^ Fintype.card m)
⊢ IsUnit (det B)
[PROOFSTEP]
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
[GOAL]
case neg.inr
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : ¬IsUnit (det B)
h✝ : Nonempty m
hAB : ¬IsUnit (det (kroneckerMap (fun x x_1 => x * x_1) A B))
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
  -- otherwise follows trivially from `mul_kronecker_mul`
[GOAL]
case pos
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : IsUnit (det B)
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
[PROOFSTEP]
apply inv_eq_right_inv
[GOAL]
case pos.h
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit (det A)
hB : IsUnit (det B)
⊢ kroneckerMap (fun x x_1 => x * x_1) A B * kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹ = 1
[PROOFSTEP]
rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ det (kroneckerMap (tmul R) A B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
refine' (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans _
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ det (map A fun a => ↑(↑(mk R α β) a) 1) ^ Fintype.card n * det (map B fun b => ↑(↑(mk R α β) 1) b) ^ Fintype.card m =
    (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
simp (config := { eta := false }) only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ det (map A fun a => ↑includeLeft a) ^ Fintype.card n * det (map B fun b => ↑includeRight b) ^ Fintype.card m =
    (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
[GOAL]
R : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
q : Type u_12
r : Type u_13
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ ↑includeLeft (det A) ^ Fintype.card n * ↑includeRight (det B) ^ Fintype.card m =
    (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)
[PROOFSTEP]
simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow, _root_.mul_one, _root_.one_mul]


[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
⊢ Set.PairwiseDisjoint (Set.range singleton) id
[PROOFSTEP]
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
a b : α
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
[PROOFSTEP]
exact disjoint_singleton.2 (ne_of_apply_ne _ h)
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (↑(Finset.image g s)) f
[PROOFSTEP]
rw [coe_image]
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (g '' ↑s) f
[PROOFSTEP]
exact hs.image_of_le hf
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
⊢ PairwiseDisjoint (⋃ (i : ι') (_ : i ∈ s), ↑(g i)) f
[PROOFSTEP]
rintro a ha b hb hab
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a : ι
ha : a ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
b : ι
hb : b ∈ ⋃ (i : ι') (_ : i ∈ s), ↑(g i)
hab : a ≠ b
⊢ (Disjoint on f) a b
[PROOFSTEP]
simp_rw [Set.mem_iUnion] at ha hb
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a b : ι
hab : a ≠ b
ha : ∃ i i_1, a ∈ ↑(g i)
hb : ∃ i i_1, b ∈ ↑(g i)
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain ⟨c, hc, ha⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a b : ι
hab : a ≠ b
hb : ∃ i i_1, b ∈ ↑(g i)
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain ⟨d, hd, hb⟩ := hb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain hcd | hcd := eq_or_ne (g c) (g d)
[GOAL]
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ (Disjoint on f) a b
[PROOFSTEP]
exact hg d hd (by rwa [hcd] at ha ) hb hab
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ a ∈ ↑(g d)
[PROOFSTEP]
rwa [hcd] at ha
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint s fun i' => sup (g i') f
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (↑(g i)) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c ≠ g d
⊢ (Disjoint on f) a b
[PROOFSTEP]
exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise (↑(toFinset l)) r
hn : Nodup l
⊢ Pairwise r l
[PROOFSTEP]
rw [coe_toFinset] at hl
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise {a | a ∈ l} r
hn : Nodup l
⊢ Pairwise r l
[PROOFSTEP]
exact hn.pairwise_of_set_pairwise hl
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
[PROOFSTEP]
letI : IsSymm α r := ⟨hs⟩
[GOAL]
α : Type u_1
ι : Type u_2
ι' : Type u_3
β : Type u_4
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
this : IsSymm α r := { symm := hs }
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
[PROOFSTEP]
rw [coe_toFinset, hn.pairwise_coe]