mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : (affineCombination k univ s.points) w ∈ s.closedInterior
hright : w i = 1 - x
⊢ False

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : (affineCombination k univ s.points) w ∈ s.closedInterior
hright : w i = 1 - x
⊢ False
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_1.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m₁ m₂ : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ •
      (MultilinearMap.domDomCongr a✝
          (MultilinearMap.domCoprod' (↑m₁ ⊗ₜ[R'] ↑n) + MultilinearMap.domCoprod' (↑m₂ ⊗ₜ[R'] ↑n)))
        x✝ =
    Perm.sign a✝ •
      ((MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m₁ ⊗ₜ[R'] ↑n))) x✝ +
        (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m₂ ⊗ₜ[R'] ↑n))) x✝)

Tactic:
]

Goal state after:
case refine_1.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m₁ m₂ : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ •
      (MultilinearMap.domDomCongr a✝
          (MultilinearMap.domCoprod' (↑m₁ ⊗ₜ[R'] ↑n) + MultilinearMap.domCoprod' (↑m₂ ⊗ₜ[R'] ↑n)))
        x✝ =
    Perm.sign a✝ •
      ((MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m₁ ⊗ₜ[R'] ↑n))) x✝ +
        (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m₂ ⊗ₜ[R'] ↑n))) x✝)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hright : w i = 1 - x
⊢ False

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hright : w i = 1 - x
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
⊢ (∀ (j : Fin n), w j ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔ (∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1) ∧ w i = 1 - x

Tactic:
]

Goal state after:
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
⊢ (∀ (j : Fin n), w j ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔ (∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1) ∧ w i = 1 - x
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_2.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝

Tactic:
]

Goal state after:
case refine_2.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : x = 1 - w i
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ x⁻¹ * w j ≤ 1

Tactic:
]

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : x = 1 - w i
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ x⁻¹ * w j ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : x = 1 - w i
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ w j + w i ≤ ∑ i, w i

Tactic:
]

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : x = 1 - w i
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ w j + w i ≤ ∑ i, w i
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_3.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ •
      (MultilinearMap.domDomCongr a✝
          (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₁) + MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₂)))
        x✝ =
    Perm.sign a✝ •
      ((MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₁))) x✝ +
        (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₂))) x✝)

Tactic:
]

Goal state after:
case refine_3.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ •
      (MultilinearMap.domDomCongr a✝
          (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₁) + MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₂)))
        x✝ =
    Perm.sign a✝ •
      ((MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₁))) x✝ +
        (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n₂))) x✝)
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_4.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝

Tactic:
]

Goal state after:
case refine_4.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
    ∃ x_1 ∈ (s.faceOpposite i).closedInterior, (homothety (s.points i) x) x_1 = (affineCombination k univ s.points) w

Tactic:
]

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
    ∃ x_1 ∈ (s.faceOpposite i).closedInterior, (homothety (s.points i) x) x_1 = (affineCombination k univ s.points) w
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: case smul
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
a : A
w : W
h :
  (ibc.toDualBaseChangeAux (1 ⊗ₜ[R] f)) w =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      w
⊢ (ibc.toDualBaseChangeAux (1 ⊗ₜ[R] f)) (a • w) =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      (a • w)

Tactic:
| smul a w h =>

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ ∑ xbar ∈ Finset.image (Quotient.mk (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) Finset.univ,
      ∑ y with ⟦y⟧ = xbar, sign y • domDomCongr y (a.domCoprod b) =
    ∑ σ, domCoprod.summand (alternatization a) (alternatization b) σ

Tactic:
]

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ ∑ xbar ∈ Finset.image (Quotient.mk (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) Finset.univ,
      ∑ y with ⟦y⟧ = xbar, sign y • domDomCongr y (a.domCoprod b) =
    ∑ σ, domCoprod.summand (alternatization a) (alternatization b) σ
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (j : Fin (n + 1)), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1) ∧ x⁻¹ * (w i - 1) + 1 = 0 ↔
    (∀ i_1 ∈ {i}ᶜ, (lineMap (Pi.single i 1) w) x⁻¹ i_1 ∈ Set.Icc 0 1) ∧
      ∀ i_1 ∉ {i}ᶜ, (lineMap (Pi.single i 1) w) x⁻¹ i_1 = 0

pp: case pos.hw
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ ∑ i_1, (lineMap (Pi.single i 1) w) x⁻¹ i_1 = 1

Tactic:
]

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (j : Fin (n + 1)), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1) ∧ x⁻¹ * (w i - 1) + 1 = 0 ↔
    (∀ i_1 ∈ {i}ᶜ, (lineMap (Pi.single i 1) w) x⁻¹ i_1 ∈ Set.Icc 0 1) ∧
      ∀ i_1 ∉ {i}ᶜ, (lineMap (Pi.single i 1) w) x⁻¹ i_1 = 0

case pos.hw
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ ∑ i_1, (lineMap (Pi.single i 1) w) x⁻¹ i_1 = 1
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
⊢ map (DistribSMul.toLinearMap R V e) W = W

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
⊢ map (DistribSMul.toLinearMap R V e) W = W
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case a
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
x : V
hx : x ∈ W
⊢ x ∈ (↑e).fixedSubmodule

Tactic:
]

Goal state after:
case a
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
x : V
hx : x ∈ W
⊢ x ∈ (↑e).fixedSubmodule
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case inr
R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Nontrivial R
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ (algebraMap R S) ((toMatrix b b) f).det = (algebraMap R S) ((toMatrix b b) f).det

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv' : e w = v
hv : w ∈ W
⊢ w ∈ W

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv' : e w = v
hv : w ∈ W
⊢ w ∈ W
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case mpr
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
H : ∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)
x : V ⧸ (↑e).fixedSubmodule
y : V
hy : (↑e).fixedSubmodule.mkQ y = x
⊢ e.fixedReduce ((↑e).fixedSubmodule.mkQ y) = a • (↑e).fixedSubmodule.mkQ y

Tactic:
]

Goal state after:
case mpr
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
H : ∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)
x : V ⧸ (↑e).fixedSubmodule
y : V
hy : (↑e).fixedSubmodule.mkQ y = x
⊢ e.fixedReduce ((↑e).fixedSubmodule.mkQ y) = a • (↑e).fixedSubmodule.mkQ y
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → f * (b.coord i).transvection (r • b j) = (b.coord i).transvection (r • b j) * f
i j : ι
hij : i ≠ j
r : R
this : ∀ (x : V), (f * (b.coord i).transvection (r • b j)) x = ((b.coord i).transvection (r • b j) * f) x
⊢ r • f (b j) = (b.coord i) (f (b i)) • r • b j

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → f * (b.coord i).transvection (r • b j) = (b.coord i).transvection (r • b j) * f
i j : ι
hij : i ≠ j
r : R
this : ∀ (x : V), (f * (b.coord i).transvection (r • b j)) x = ((b.coord i).transvection (r • b j) * f) x
⊢ r • f (b j) = (b.coord i) (f (b i)) • r • b j
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
⊢ (Fintype.card ιa).factorial • (Fintype.card ιb).factorial • AlternatingMap.domCoprod' (a ⊗ₜ[R'] b) =
    (Fintype.card ιa).factorial • (Fintype.card ιb).factorial • AlternatingMap.domCoprod' (a ⊗ₜ[R'] b)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
⊢ ((b.repr x).sum fun a b_1 ↦ f (b_1 • b a)) = (⟨(b.coord i) (f (b i)), ⋯⟩ • 1) ((b.repr x).sum fun i a ↦ a • b i)

Tactic:
]

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
⊢ ((b.repr x).sum fun a b_1 ↦ f (b_1 • b a)) = (⟨(b.coord i) (f (b i)), ⋯⟩ • 1) ((b.repr x).sum fun i a ↦ a • b i)
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
i : ι
⊢ ∀ (i_1 : ι), (b.repr (f (b i))) i_1 = (b.repr ((b.coord i) (f (b i)) • b i)) i_1

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
i : ι
⊢ ∀ (i_1 : ι), (b.repr (f (b i))) i_1 = (b.repr ((b.coord i) (f (b i)) • b i)) i_1
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : ∀ (i_1 : ι), (b.repr (s • b i + t • f (b i))) i_1 = (b.repr 0) i_1
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
⊢ t = 0 ∨ (b.repr (f (b i))) j = 0

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : ∀ (i_1 : ι), (b.repr (s • b i + t • f (b i))) i_1 = (b.repr 0) i_1
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
⊢ t = 0 ∨ (b.repr (f (b i))) j = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv : f (b i) * (b.repr v) i = 0
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ f x • v = 0

Tactic:
]

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv : f (b i) * (b.repr v) i = 0
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ f x • v = 0