ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).hom.app K).f n = (XIsoOfEq K ⋯).hom
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁶ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : SMulWithZero ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module ℝ M<VAR>φ : ι → X → M<GOAL>∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁶ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : SMulWithZero ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module ℝ M<VAR>φ : ι → X → M<GOAL>(support fun i => (ρ i) x₀ • φ i x₀) ⊆ ↑(ρ.finsupport x₀)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁶ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : SMulWithZero ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module ℝ M<VAR>φ : ι → X → M<VAR>this : (fun i => (ρ i) x₀ • φ i x₀) = (fun i => (ρ i) x₀) • fun i => φ i x₀<GOAL>(support fun i => (ρ i) x₀ • φ i x₀) ⊆ ↑(ρ.finsupport x₀)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁶ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : SMulWithZero ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module ℝ M<VAR>φ : ι → X → M<VAR>this : (fun i => (ρ i) x₀ • φ i x₀) = (fun i => (ρ i) x₀) • fun i => φ i x₀<GOAL>((support fun i => (ρ i) x₀) ∩ support fun i => φ i x₀) ⊆ support fun i => (ρ i) x₀
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype m<VAR>i : n<VAR>j : m<VAR>c : α<VAR>x : m → α<VAR>i' : n<GOAL>(∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i'
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype m<VAR>i : n<VAR>j : m<VAR>c : α<VAR>x : m → α<GOAL>(∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype m<VAR>i : n<VAR>j : m<VAR>c : α<VAR>x : m → α<VAR>i' : n<VAR>h : i ≠ i'<GOAL>(∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i'
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Semiring α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>r : α<VAR>M : Matrix n n α<GOAL>Commute ((scalar n) r) M ↔ r • M = MulOpposite.op r • M
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : s ∈ 𝒜<GOAL>s.erase a ∈ 𝓓 a 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : s ∈ 𝒜<GOAL>s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : s ∈ 𝒜<VAR>h : s.erase a ∉ 𝒜<GOAL>insert a (s.erase a) ∈ 𝒜
<VAR>a✝ b✝ m n p a b : ℕ<VAR>hab : a.Coprime b<VAR>q : ℕ<GOAL>(a * b).factorization q = (a.factorization + b.factorization) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>η : Type u_5<VAR>ε : Type u_6<VAR>e : PartialEquiv α β<VAR>f : PartialEquiv β γ<VAR>e' : PartialEquiv δ η<VAR>f' : PartialEquiv η ε<GOAL>(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>η : Type u_5<VAR>ε : Type u_6<VAR>e : PartialEquiv α β<VAR>f : PartialEquiv β γ<VAR>e' : PartialEquiv δ η<VAR>f' : PartialEquiv η ε<VAR>x : α<VAR>y : δ<GOAL>(x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔ (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<GOAL>(∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P'<VAR>x : P<GOAL>x ∈ (canonicalEquiv S P P').symm I ↔ x ∈ (canonicalEquiv S P' P) I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P'<VAR>x : P<GOAL>(∃ x_1 ∈ I, ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm x_1 = x) ↔ ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>s : Set β<VAR>hs : s.Finite<VAR>f : β → α<GOAL>Multipliable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>s : Set β<VAR>hs : s.Finite<VAR>f : β → α<VAR>this : Multipliable (f ∘ Subtype.val)<GOAL>Multipliable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<VAR>s : Set α<GOAL>mulSupport f = s ↔ (∀ x ∈ s, f x ≠ 1) ∧ ∀ x ∉ s, f x = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a : ℤ<GOAL>(shiftAddHom K L n a) (-γ) = -γ.shift a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>F : Filter β<VAR>x : α<GOAL>x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>F : Filter β<VAR>x : α<GOAL>(∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<GOAL>IsOpen {x | CPolynomialAt 𝕜 f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<GOAL>∀ x ∈ {x | CPolynomialAt 𝕜 f x}, {x | CPolynomialAt 𝕜 f x} ∈ 𝓝 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>x✝ y x : E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hr : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>{x | CPolynomialAt 𝕜 f x} ∈ 𝓝 x
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : NonAssocRing R<VAR>v : V<VAR>vec : V → R<GOAL>(lapMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(ghostComponent (n + 1)) x.verschiebungFun = ↑p * (ghostComponent n) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.verschiebungFun.coeff i ^ p ^ (n + 1 - i) = ↑p * ∑ i ∈ Finset.range (n + 1), ↑p ^ i * x.coeff i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>∀ x_1 ∈ Finset.range (n + 1), ↑p ^ (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) = ↑p * (↑p ^ x_1 * x.coeff x_1 ^ p ^ (n - x_1))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<VAR>n i : ℕ<GOAL>↑p ^ (i + 1) * x.verschiebungFun.coeff (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>p : ι → Prop<VAR>U : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p U<VAR>s : Set α<VAR>x : α<GOAL>x ∈ ⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i) ↔ x ∈ closure s
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>a : AdjoinRoot (minpoly R x)<GOAL>(aeval ⟨x, ⋯⟩) (minpoly R x) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<GOAL>coroot k = coroot l
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<GOAL>coroot k = coroot l
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<GOAL>p.toLin.flip (coroot k) = p.toLin.flip (coroot l)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<VAR>_i : NoZeroSMulDivisors ℤ M<GOAL>p.toLin.flip (coroot k) = p.toLin.flip (coroot l)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<VAR>_i : NoZeroSMulDivisors ℤ M<VAR>this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.toLin.flip ∘ ⇑coroot))<GOAL>p.toLin.flip (coroot k) = p.toLin.flip (coroot l)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p.toLin (root i)))) (range ⇑coroot) (range ⇑coroot)<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<VAR>l : ι<VAR>hl : coroot l = (preReflection (coroot i) (p.toLin (root i))) (coroot j)<VAR>hkl : (p.toLin.flip (coroot l)) (root k) = 2<VAR>_i : NoZeroSMulDivisors ℤ M<VAR>this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.toLin.flip ∘ ⇑coroot))<GOAL>(span R (range ⇑root)).subtype.dualMap ((⇑p.toLin.flip ∘ ⇑coroot) k) = (span R (range ⇑root)).subtype.dualMap ((⇑p.toLin.flip ∘ ⇑coroot) l)