awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1
s : Set ι
hm :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s))
    ((affineCombination k fs p : (a : ι → k) → P) w : P)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : (↑fs' : Set ι) ⊆ s
hw' : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 1
he :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs p : (a : ι → k) → P) w : P)
    ((affineCombination k fs' p : (a : ι → k) → P) w' : P)
hi' : (↑fs : Set ι).indicator w i = 0
⊢ i ∈ (↑fs : Set ι) → w i = 0

Tactic:
rw [Set.indicator_apply_eq_zero] at hi'

Premises used: Set.indicator_apply_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1
s : Set ι
hm :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s))
    ((affineCombination k fs p : (a : ι → k) → P) w : P)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : (↑fs' : Set ι) ⊆ s
hw' : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 1
he :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs p : (a : ι → k) → P) w : P)
    ((affineCombination k fs' p : (a : ι → k) → P) w' : P)
hi' : i ∈ (↑fs : Set ι) → w i = 0
⊢ w i = 0

Tactic:
hi' (Finset.mem_coe.2 hifs)

Premises used: Iff.mpr, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1
s : Set ι
hm :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s))
    ((affineCombination k fs p : (a : ι → k) → P) w : P)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : (↑fs' : Set ι) ⊆ s
hw' : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 1
he :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs p : (a : ι → k) → P) w : P)
    ((affineCombination k fs' p : (a : ι → k) → P) w' : P)
hi' : i ∈ (↑fs : Set ι) → w i = 0
⊢ w i = 0

Tactic:
exact hi' (Finset.mem_coe.2 hifs)

Premises used: Iff.mpr, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) w₂ : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
⊢ comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂

Tactic:
have hw₂e : extend e w₂ 0 ∘ e = w₂ := extend_comp e.injective _ _
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) w₂ : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)

Tactic:
rw [← hw₂e, ← affineCombination_map] at h

Premises used: Finset.affineCombination_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) w₂ : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
h₁ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
⊢ comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂

Tactic:
rw [← hw₂e, ← affineCombination_map] at h

Premises used: Finset.affineCombination_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ (↑(map e s₂) : Set ι).indicator (extend (⇑e : (a : ι₂) → ι) w₂ 0) = (↑s₁ : Set ι).indicator w₁

Tactic:
(ha.indicator_eq_of_affineCombination_eq s₁ (s₂.map e) _ _ hw₁ ?_ h.symm).symm

Premises used: AffineIndependent.indicator_eq_of_affineCombination_eq, Finset.map, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
refine : Eq.{u_1 + 1} (α := k) (∑ i ∈ map e s₂, extend (⇑e : (a : ι₂) → ι) w₂ 0 i) 1
⊢ (↑(map e s₂) : Set ι).indicator (extend (⇑e : (a : ι₂) → ι) w₂ 0) = (↑s₁ : Set ι).indicator w₁

Tactic:
refine (ha.indicator_eq_of_affineCombination_eq s₁ (s₂.map e) _ _ hw₁ ?_ h.symm).symm

Premises used: AffineIndependent.indicator_eq_of_affineCombination_eq, Finset.map, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
rw :
  Eq.{u_1 + 1} (α := k)
    (∑ x ∈ s₂,
      extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
        ((e : (a : ι₂) → ι) x : ι))
    1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ map e s₂, extend (⇑e : (a : ι₂) → ι) w₂ 0 i) 1

Tactic:
rw [sum_map]

Premises used: Finset.sum_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1

Tactic:
hw₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
h₁ :
  ∀ (i : ι₂) (hi : i ∈ s₂),
    extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
        ((e : (a : ι₂) → ι) i : ι) =
      w₂ i
⊢ Eq.{u_1 + 1} (α := k)
    (∑ x ∈ s₂,
      extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
        ((e : (a : ι₂) → ι) x : ι))
    1

Tactic:
convert! hw₂ with i hi
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
i : ι₂
hi : i ∈ s₂
⊢ extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
      ((e : (a : ι₂) → ι) i : ι) =
    w₂ i

Tactic:
e.injective.extend_apply _ _ _

Premises used: Function.Injective.extend_apply, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
i : ι₂
hi : i ∈ s₂
⊢ extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
      ((e : (a : ι₂) → ι) i : ι) =
    w₂ i

Tactic:
exact e.injective.extend_apply _ _ _

Premises used: Function.Injective.extend_apply, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Fintype ι
ι₂ : Type u_5
inst_5 : Fintype ι₂
p : ι → P
ha : AffineIndependent k p
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i : ι, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i : ι₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k univ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) w₂ : P)
    ((affineCombination k univ p : (a : ι → k) → P) w₁ : P)
⊢ Set.indicator (Set.range.{u_4, u_5 + 1} (ι := ι₂) (⇑e : (a : ι₂) → ι)) (extend (⇑e : (a : ι₂) → ι) w₂ 0) = w₁

Tactic:
simpa using ha.indicator_extend_eq_of_affineCombination_comp_embedding_eq hw₁ hw₂ e h

Premises used: AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
inl : ∀ (h : IsEmpty ι), AffineIndependent k p
inr : ∀ (h : Nonempty ι), AffineIndependent k p
⊢ AffineIndependent k p

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
h : IsEmpty ι
⊢ AffineIndependent k p

Tactic:
apply affineIndependent_of_subsingleton

Premises used: affineIndependent_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
h : Nonempty ι
inr : ∀ (i : ι), AffineIndependent k p
⊢ AffineIndependent k p

Tactic:
obtain ⟨i⟩ := h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
i : ι
inr : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
⊢ AffineIndependent k p

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k p i]

Premises used: affineIndependent_iff_linearIndependent_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
i : ι
⊢ LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)

Tactic:
simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub] at hai

Premises used: Function.comp, AffineMap.linearMap_vsub, affineIndependent_iff_linearIndependent_vsub, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
i : ι
hai :
  LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i

Tactic:
LinearIndependent.of_comp f.linear hai

Premises used: LinearIndependent.of_comp, AffineMap.linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
i : ι
hai :
  LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i

Tactic:
exact LinearIndependent.of_comp f.linear hai

Premises used: LinearIndependent.of_comp, AffineMap.linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
inl : ∀ (h : IsEmpty ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
inr : ∀ (h : Nonempty ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
h : IsEmpty ι
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)

Tactic:
apply affineIndependent_of_subsingleton

Premises used: affineIndependent_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
h : Nonempty ι
inr : ∀ (i : ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)

Tactic:
obtain ⟨i⟩ := h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k p i] at hai

Premises used: affineIndependent_iff_linearIndependent_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
inr :
  LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)

Tactic:
simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub]

Premises used: Function.comp, AffineMap.linearMap_vsub, affineIndependent_iff_linearIndependent_vsub, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
rwa : Injective.{u_2 + 1, u_5 + 1} (α := V) (β := V₂) (⇑f.linear : (a : V) → V₂)
rwa₁ rwa₂ rwa₃ rwa₄ : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ f.linear.ker = ⊥

Tactic:
rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]

Premises used: LinearMap.ker_eq_bot, AffineMap.linear_injective_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
⊢ f.linear.ker = ⊥

Tactic:
have hf' : LinearMap.ker f.linear = ⊥ := by rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
hf' : f.linear.ker = ⊥
⊢ LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)

Tactic:
LinearIndependent.map' hai f.linear hf'

Premises used: LinearIndependent.map', AffineMap.linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
hf' : f.linear.ker = ⊥
⊢ LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)

Tactic:
exact LinearIndependent.map' hai f.linear hf'

Premises used: LinearIndependent.map', AffineMap.linear