ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>f : R →ₙ+* S<VAR>g : R →ₙ+* T<GOAL>(NonUnitalRingHom.fst S T).comp (f.prod g) = f
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>f : R →ₙ+* S<VAR>g : R →ₙ+* T<GOAL>(NonUnitalRingHom.snd S T).comp (f.prod g) = g
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring T<VAR>f : R →ₙ+* S × T<GOAL>((NonUnitalRingHom.fst S T).comp f).prod ((NonUnitalRingHom.snd S T).comp f) = f
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring R'<VAR>NonUnitalNonAssocSemiring S'<VAR>f : R →ₙ+* R'<VAR>g : S →ₙ+* S'<GOAL>f.prodMap g = (f.comp (NonUnitalRingHom.fst R S)).prod (g.comp (NonUnitalRingHom.snd R S))
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring R'<VAR>NonUnitalNonAssocSemiring S'<VAR>f : R →ₙ+* R'<VAR>g : S →ₙ+* S'<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring R'<VAR>NonUnitalNonAssocSemiring S'<VAR>NonUnitalNonAssocSemiring T<VAR>f : T →ₙ+* R<VAR>g : T →ₙ+* S<VAR>f' : R →ₙ+* R'<VAR>g' : S →ₙ+* S'<GOAL>(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>⇑(RingHom.fst R S) = Prod.fst
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>⇑(RingHom.snd R S) = Prod.snd
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>f : R →+* S<VAR>g : R →+* T<VAR>x : R<GOAL>(f.prod g) x = (f x, g x)
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>f : R →+* S<VAR>g : R →+* T<GOAL>(RingHom.fst S T).comp (f.prod g) = f
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>f : R →+* S<VAR>g : R →+* T<GOAL>(RingHom.snd S T).comp (f.prod g) = g
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>T : Type u_7<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>f : R →+* S × T<GOAL>((RingHom.fst S T).comp f).prod ((RingHom.snd S T).comp f) = f
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<VAR>f : R →+* R'<VAR>g : S →+* S'<GOAL>f.prodMap g = (f.comp (RingHom.fst R S)).prod (g.comp (RingHom.snd R S))
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<VAR>f : R →+* R'<VAR>g : S →+* S'<GOAL>⇑(f.prodMap g) = Prod.map ⇑f ⇑g
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<VAR>NonAssocSemiring T<VAR>f : T →+* R<VAR>g : T →+* S<VAR>f' : R →+* R'<VAR>g' : S →+* S'<GOAL>(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>⇑RingEquiv.prodComm = Prod.swap
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>⇑RingEquiv.prodComm.symm = Prod.swap
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>(RingHom.fst S R).comp ↑RingEquiv.prodComm = RingHom.snd R S
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>(RingHom.snd S R).comp ↑RingEquiv.prodComm = RingHom.fst R S
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<VAR>rrss : (R × R') × S × S'<GOAL>(RingEquiv.prodProdProdComm R R' S S') rrss = ((rrss.1.1, rrss.2.1), rrss.1.2, rrss.2.2)
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<GOAL>(RingEquiv.prodProdProdComm R R' S S').symm = RingEquiv.prodProdProdComm R S R' S'
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<GOAL>↑(RingEquiv.prodProdProdComm R R' S S') = AddEquiv.prodProdProdComm R R' S S'
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<GOAL>↑(RingEquiv.prodProdProdComm R R' S S') = MulEquiv.prodProdProdComm R R' S S'
<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring R'<VAR>NonAssocSemiring S'<GOAL>↑(RingEquiv.prodProdProdComm R R' S S') = Equiv.prodProdProdComm R R' S S'
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>Subsingleton S<VAR>self : R × S<GOAL>(RingEquiv.prodZeroRing R S).symm self = self.1
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>Subsingleton S<VAR>x : R<GOAL>(RingEquiv.prodZeroRing R S) x = (x, 0)
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>Subsingleton S<VAR>x : R<GOAL>(RingEquiv.zeroRingProd R S) x = (0, x)
<VAR>R : Type u_3<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>Subsingleton S<VAR>self : S × R<GOAL>(RingEquiv.zeroRingProd R S).symm self = self.2
<VAR>R : Type u_9<VAR>S : Type u_10<VAR>Ring R<VAR>Ring S<VAR>IsDomain (R × S)<VAR>Nontrivial R<VAR>Nontrivial S<GOAL>False
<VAR>α : Type u<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a : α<VAR>Invertible a<VAR>Invertible (-a)<GOAL>⅟(-a) = -⅟a
<VAR>α : Type u<VAR>Ring α<VAR>Invertible 2<GOAL>1 - ⅟2 = ⅟2
<VAR>α : Type u<VAR>NonAssocSemiring α<VAR>Invertible 2<GOAL>⅟2 + ⅟2 = 1
<VAR>α : Type u<VAR>Semiring α<VAR>Nontrivial α<VAR>n : ℕ<VAR>Invertible ↑n<GOAL>0 < n
<VAR>α : Type u<VAR>Semiring α<VAR>a b : α<VAR>Invertible a<VAR>Invertible b<GOAL>⅟a + ⅟b = ⅟a * (a + b) * ⅟b
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>Invertible a<VAR>Invertible b<GOAL>⅟a - ⅟b = ⅟a * (b - a) * ⅟b
<VAR>α : Type u<VAR>Semiring α<VAR>a b : α<VAR>h : IsUnit a ↔ IsUnit b<GOAL>Ring.inverse a + Ring.inverse b = Ring.inverse a * (a + b) * Ring.inverse b
<VAR>α : Type u<VAR>Ring α<VAR>a b : α<VAR>h : IsUnit a ↔ IsUnit b<GOAL>Ring.inverse a - Ring.inverse b = Ring.inverse a * (b - a) * Ring.inverse b
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>Subsingleton G<GOAL>UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>Subsingleton G<GOAL>UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<VAR>hA1 : A.card ≤ 1<VAR>hB1 : B.card ≤ 1<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<VAR>hA1 : A.card ≤ 1<VAR>hB1 : B.card ≤ 1<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueAdd A B a b
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<VAR>a b : G<GOAL>a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueAdd A B a0 b0<VAR>a b : G<GOAL>a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<GOAL>Subsingleton { ab // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0 }
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueAdd A B a0 b0<GOAL>Subsingleton { ab // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 + ab.2 = a0 + b0 }
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<GOAL>{ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueAdd A B a0 b0<GOAL>{ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 + ab.2 = a0 + b0}.Subsingleton
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>aA : a0 ∈ A<VAR>bB : b0 ∈ B<GOAL>UniqueAdd A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 + ab.2 = a0 + b0
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>aA : a0 ∈ A<VAR>bB : b0 ∈ B<GOAL>UniqueMul A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>DecidableEq G<VAR>ha0 : a0 ∈ A<VAR>hb0 : b0 ∈ B<GOAL>UniqueAdd A B a0 b0 ↔ (Finset.filter (fun p => p.1 + p.2 = a0 + b0) (A ×ˢ B)).card ≤ 1
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>DecidableEq G<VAR>ha0 : a0 ∈ A<VAR>hb0 : b0 ∈ B<GOAL>UniqueMul A B a0 b0 ↔ (Finset.filter (fun p => p.1 * p.2 = a0 * b0) (A ×ˢ B)).card ≤ 1
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<GOAL>(∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<GOAL>(∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 + ab.2 = g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>f : AddHom G H<VAR>hf : Function.Injective ⇑f<VAR>a0 b0 : G<VAR>A B : Finset H<VAR>u : UniqueAdd A B (f a0) (f b0)<GOAL>UniqueAdd (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Mul G<VAR>Mul H<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>a0 b0 : G<VAR>A B : Finset H<VAR>u : UniqueMul A B (f a0) (f b0)<GOAL>UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Mul G<VAR>Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>h : UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0)<GOAL>UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>DecidableEq H<VAR>f : AddHom G H<VAR>hf : ∀ ⦃a b c d : G⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>h : UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0)<GOAL>UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Mul G<VAR>Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<GOAL>UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>DecidableEq H<VAR>f : AddHom G H<VAR>hf : Function.Injective ⇑f<GOAL>UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>f : G ↪ H<VAR>mul : ∀ (x y : G), f (x + y) = f x + f y<GOAL>UniqueAdd (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Mul G<VAR>Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>f : G ↪ H<VAR>mul : ∀ (x y : G), f (x * y) = f x * f y<GOAL>UniqueMul (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0)<GOAL>UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A) (AddOpposite.op b0) (AddOpposite.op a0)<GOAL>UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueAdd A B a0 b0<GOAL>UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A) (AddOpposite.op b0) (AddOpposite.op a0)
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<GOAL>UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0)
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>a0 b0 : G<GOAL>UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0) ↔ UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>a0 b0 : G<GOAL>UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A) (AddOpposite.op b0) (AddOpposite.op a0) ↔ UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>DecidableEq H<VAR>f : AddHom G H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huH : UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) aH bH<VAR>huG : UniqueAdd (Finset.filter (fun x => f x = aH) A) (Finset.filter (fun x => f x = bH) B) aG bG<GOAL>UniqueAdd A B aG bG
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Mul G<VAR>Mul H<VAR>DecidableEq H<VAR>f : G →ₙ* H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huH : UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) aH bH<VAR>huG : UniqueMul (Finset.filter (fun x => f x = aH) A) (Finset.filter (fun x => f x = bH) B) aG bG<GOAL>UniqueMul A B aG bG
<VAR>G : Type u_1<VAR>Add G<VAR>self : UniqueSums G<VAR>A B : Finset G<GOAL>A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueAdd A B a0 b0
<VAR>G : Type u_1<VAR>Mul G<VAR>self : UniqueProds G<VAR>A B : Finset G<GOAL>A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>Add G<VAR>self : TwoUniqueSums G<VAR>A B : Finset G<GOAL>1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2
<VAR>G : Type u_1<VAR>Mul G<VAR>self : TwoUniqueProds G<VAR>A B : Finset G<GOAL>1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G : Type u_1<VAR>Mul G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>Add G<VAR>A B : Finset G<VAR>h : 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueAdd A B a b
<VAR>G : Type u<VAR>H : Type v<VAR>Add G<VAR>Add H<VAR>f : AddHom H G<VAR>hf : ∀ ⦃a b c d : H⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>UniqueSums G<GOAL>UniqueSums H
<VAR>G : Type u<VAR>H : Type v<VAR>Mul G<VAR>Mul H<VAR>f : H →ₙ* G<VAR>hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>UniqueProds G<GOAL>UniqueProds H
<VAR>G : Type u<VAR>H : Type v<VAR>Add G<VAR>Add H<VAR>f : AddHom H G<VAR>hf : Function.Injective ⇑f<GOAL>UniqueSums G → UniqueSums H
<VAR>G : Type u<VAR>H : Type v<VAR>Mul G<VAR>Mul H<VAR>f : H →ₙ* G<VAR>hf : Function.Injective ⇑f<GOAL>UniqueProds G → UniqueProds H
<VAR>G : Type u<VAR>H : Type v<VAR>Add G<VAR>Add H<VAR>f : G ≃+ H<GOAL>UniqueSums G ↔ UniqueSums H
<VAR>G : Type u<VAR>H : Type v<VAR>Mul G<VAR>Mul H<VAR>f : G ≃* H<GOAL>UniqueProds G ↔ UniqueProds H
<VAR>G : Type u<VAR>Mul G<VAR>h : UniqueProds Gᵐᵒᵖ<GOAL>UniqueProds G
<VAR>G : Type u<VAR>Add G<VAR>h : UniqueSums Gᵃᵒᵖ<GOAL>UniqueSums G
<VAR>G : Type u<VAR>Add G<VAR>UniqueSums G<GOAL>IsLeftCancelAdd G
<VAR>G : Type u<VAR>Mul G<VAR>UniqueProds G<GOAL>IsLeftCancelMul G
<VAR>G : Type u<VAR>Add G<VAR>UniqueSums G<GOAL>IsCancelAdd G
<VAR>G : Type u<VAR>Mul G<VAR>UniqueProds G<GOAL>IsCancelMul G
<VAR>G : Type u_1<VAR>AddSemigroup G<VAR>IsCancelAdd G<VAR>h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueAdd A A a1 a2<GOAL>UniqueSums G
<VAR>G : Type u_1<VAR>Semigroup G<VAR>IsCancelMul G<VAR>h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2<GOAL>UniqueProds G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>UniqueSums G<GOAL>TwoUniqueSums G
<VAR>G : Type u_1<VAR>Group G<VAR>UniqueProds G<GOAL>TwoUniqueProds G
<VAR>G : Type u<VAR>H : Type v<VAR>Mul G<VAR>Mul H<VAR>f : H →ₙ* G<VAR>hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>TwoUniqueProds G<GOAL>TwoUniqueProds H
<VAR>G : Type u<VAR>H : Type v<VAR>Add G<VAR>Add H<VAR>f : AddHom H G<VAR>hf : ∀ ⦃a b c d : H⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>TwoUniqueSums G<GOAL>TwoUniqueSums H
<VAR>G : Type u<VAR>H : Type v<VAR>Add G<VAR>Add H<VAR>f : AddHom H G<VAR>hf : Function.Injective ⇑f<GOAL>TwoUniqueSums G → TwoUniqueSums H
<VAR>G : Type u<VAR>H : Type v<VAR>Mul G<VAR>Mul H<VAR>f : H →ₙ* G<VAR>hf : Function.Injective ⇑f<GOAL>TwoUniqueProds G → TwoUniqueProds H
<VAR>G : Type u<VAR>H : Type v<VAR>Add G<VAR>Add H<VAR>f : G ≃+ H<GOAL>TwoUniqueSums G ↔ TwoUniqueSums H
<VAR>G : Type u<VAR>H : Type v<VAR>Mul G<VAR>Mul H<VAR>f : G ≃* H<GOAL>TwoUniqueProds G ↔ TwoUniqueProds H
<VAR>G : Type u<VAR>Add G<VAR>h : TwoUniqueSums Gᵃᵒᵖ<GOAL>TwoUniqueSums G
<VAR>G : Type u<VAR>Mul G<VAR>h : TwoUniqueProds Gᵐᵒᵖ<GOAL>TwoUniqueProds G
<VAR>R : Type u_4<VAR>Semiring R<VAR>σ : R →+* R<VAR>self : RingHomId σ<GOAL>σ = RingHom.id R
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : outParam (R₁ →+* R₃)<VAR>self : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<GOAL>σ₂₃.comp σ₁₂ = σ₁₃
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>x : R₁<GOAL>σ₂₃ (σ₁₂ x) = σ₁₃ x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ : R₁ →+* R₂<VAR>σ' : outParam (R₂ →+* R₁)<VAR>self : RingHomInvPair σ σ'<GOAL>σ.comp σ' = RingHom.id R₂
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ : R₁ →+* R₂<VAR>σ' : outParam (R₂ →+* R₁)<VAR>self : RingHomInvPair σ σ'<GOAL>RingHom.comp σ' σ = RingHom.id R₁
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>RingHomInvPair σ σ'<VAR>x : R₁<GOAL>σ' (σ x) = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>RingHomInvPair σ σ'<VAR>x : R₂<GOAL>σ (σ' x) = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>e : R₁ ≃+* R₂<GOAL>RingHomInvPair ↑e ↑e.symm
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<GOAL>RingHomInvPair σ₂₁ σ₁₂
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ : R₁ →+* R₂<VAR>self : RingHomSurjective σ<GOAL>Function.Surjective ⇑σ
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ : R₁ →+* R₂<VAR>t : RingHomSurjective σ<GOAL>Function.Surjective ⇑σ
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomSurjective σ₁₂<VAR>RingHomSurjective σ₂₃<GOAL>RingHomSurjective σ₁₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>Mul β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>Mul α<VAR>Add α<VAR>LeftDistribClass α<VAR>add : ∀ (x y : β), f (x + y) = f x + f y<VAR>mul : ∀ (x y : β), f (x * y) = f x * f y<GOAL>LeftDistribClass β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>Mul β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>Mul α<VAR>Add α<VAR>RightDistribClass α<VAR>add : ∀ (x y : β), f (x + y) = f x + f y<VAR>mul : ∀ (x y : β), f (x * y) = f x * f y<GOAL>RightDistribClass β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>Mul β<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>Mul α<VAR>Add α<VAR>LeftDistribClass α<VAR>add : ∀ (x y : α), f (x + y) = f x + f y<VAR>mul : ∀ (x y : α), f (x * y) = f x * f y<GOAL>LeftDistribClass β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>Mul β<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>Mul α<VAR>Add α<VAR>RightDistribClass α<VAR>add : ∀ (x y : α), f (x + y) = f x + f y<VAR>mul : ∀ (x y : α), f (x * y) = f x * f y<GOAL>RightDistribClass β
<VAR>M : Type u_1<VAR>S : Set M<VAR>a b : M<VAR>Distrib M<VAR>ha : a ∈ S.centralizer<VAR>hb : b ∈ S.centralizer<GOAL>a + b ∈ S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>a : M<VAR>Mul M<VAR>HasDistribNeg M<VAR>ha : a ∈ S.centralizer<GOAL>-a ∈ S.centralizer
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥A<VAR>Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥B<VAR>Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥A<VAR>Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>FiniteDimensional.finrank R ↥(A ⊔ B) = FiniteDimensional.finrank R ↥A * FiniteDimensional.finrank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥B<VAR>Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<GOAL>FiniteDimensional.finrank R ↥(A ⊔ B) = FiniteDimensional.finrank R ↥B * FiniteDimensional.finrank ↥B ↥(Algebra.adjoin ↥B ↑A)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥A<VAR>Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>FiniteDimensional.finrank R ↥A ∣ FiniteDimensional.finrank R ↥(A ⊔ B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A B : Subalgebra R S<VAR>Module.Free R ↥B<VAR>Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<GOAL>FiniteDimensional.finrank R ↥B ∣ FiniteDimensional.finrank R ↥(A ⊔ B)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>x ∈ 1 ↔ ∃ y, (algebraMap R A) y = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>1 = LinearMap.range (Algebra.linearMap R A)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>1 ≤ Submodule.toAddSubmonoid 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>x ∈ 1 ↔ ∃ y, (algebraMap R A) y = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>Submodule.toSubMulAction 1 = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>1 = Submodule.span R {1}
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>1 = Submodule.span R 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>P : Submodule R A<GOAL>1 ≤ P ↔ 1 ∈ P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>A' : Type u_1<VAR>Semiring A'<VAR>Algebra R A'<VAR>f : A →ₐ[R] A'<GOAL>Submodule.map f.toLinearMap 1 = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R)) 1 = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>Submodule.comap (↑(MulOpposite.opLinearEquiv R)) 1 = 1