ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ : Finmap β<VAR>s₁ s₂ : AList β<VAR>h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries<GOAL>⟦s₁⟧ = ⟦s₂⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ : Finmap β<VAR>s₁ s₂ : AList β<VAR>h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries<GOAL>s₁.entries ~ s₂.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ : Finmap β<VAR>s₁ s₂ : AList β<VAR>h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries<GOAL>∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ : Finmap β<VAR>s₁ s₂ : AList β<VAR>h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries<VAR>x : α<VAR>y : β x<GOAL>y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>g : β → α<VAR>hg : InjOn g (mulSupport (f ∘ g))<GOAL>∏ᶠ (i : α) (_ : i ∈ range g), f i = ∏ᶠ (j : β), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>g : β → α<VAR>hg : InjOn g (mulSupport (f ∘ g))<GOAL>InjOn g (univ ∩ mulSupport (f ∘ g))
<VAR>n : ℕ<GOAL>antidiagonal (n + 2) = cons (0, n + 2) (cons (n + 2, 0) (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯) ⋯
<VAR>n : ℕ<GOAL>cons (0, n + 1 + 1) (cons (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (n + 1, 0)) (map (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }).trans ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))) (antidiagonal n)) ⋯) ⋯ = cons (0, n + 2) (cons (n + 2, 0) (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯) ⋯
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<GOAL>ContMDiffOn I' I n (fun x => f x / g x) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<GOAL>ContMDiffOn I' I n (fun x => f x * (g x)⁻¹) s
<VAR>n : ℕ<GOAL>n < 2 ^ n.size
<VAR>n : ℕ<GOAL>n < 1 <<< n.size
<VAR>n✝ : ℕ<VAR>this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size<VAR>b : Bool<VAR>n : ℕ<VAR>IH : n < 1 <<< n.size<VAR>h : ¬bit b n = 0<GOAL>bit b n < 1 <<< (bit b n).size
<VAR>n✝ : ℕ<VAR>this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size<VAR>b : Bool<VAR>n : ℕ<VAR>IH : n < 1 <<< n.size<VAR>h : ¬bit b n = 0<GOAL>bit b n < 2 * 2 ^ n.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>hf : Bijective f<VAR>s : ι → Set α<GOAL>f '' ⋂ i, s i = ⋂ i, f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>hf : Bijective f<VAR>s : ι → Set α<VAR>h✝ : IsEmpty ι<GOAL>f '' ⋂ i, s i = ⋂ i, f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>hf : Bijective f<VAR>s : ι → Set α<VAR>h✝ : Nonempty ι<GOAL>f '' ⋂ i, s i = ⋂ i, f '' s i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>r : R<VAR>f g : M →ₗ[R] N<VAR>x✝ : M<GOAL>((AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ = ((AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x✝ y : α<VAR>m n✝ : ℕ<VAR>f : α → α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>x : α<VAR>hx : x ∈ ptsOfPeriod f n<GOAL>f (f^[n.pred] x) = x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : (i : ι) → κ i → α<GOAL>⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b✝ c : β<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>b : β<GOAL>b ∈ filter p (image f s) ↔ b ∈ image f (filter (fun a => p (f a)) s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b✝ c : β<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>b : β<GOAL>(∃ a ∈ s, f a = b) ∧ p b ↔ ∃ a, (a ∈ s ∧ p (f a)) ∧ f a = b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_4, u_2} D<VAR>e : C ≌ D<VAR>B : C<VAR>α : Type u_3<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>W : D<VAR>ε : (a : α) → e.functor.obj (X a) ⟶ W<VAR>h : ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)), g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂<VAR>Z : C<VAR>a₁ a₂ : α<VAR>g₁ : Z ⟶ X a₁<VAR>g₂ : Z ⟶ X a₂<VAR>hg : g₁ ≫ π a₁ = g₂ ≫ π a₂<VAR>this : e.functor.map g₁ ≫ e.functor.map (π a₁) = e.functor.map g₂ ≫ e.functor.map (π a₂) → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂<GOAL>g₁ ≫ (fun a => e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁ = g₂ ≫ (fun a => e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_4, u_2} D<VAR>e : C ≌ D<VAR>B : C<VAR>α : Type u_3<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>W : D<VAR>ε : (a : α) → e.functor.obj (X a) ⟶ W<VAR>h : ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)), g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂<VAR>Z : C<VAR>a₁ a₂ : α<VAR>g₁ : Z ⟶ X a₁<VAR>g₂ : Z ⟶ X a₂<VAR>hg : g₁ ≫ π a₁ = g₂ ≫ π a₂<VAR>this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂<GOAL>g₁ ≫ (fun a => e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁ = g₂ ≫ (fun a => e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>(f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>(f z - f x) * (z - y) ≤ (f z - f y) * (z - x)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<GOAL>x ∈ (base φ).range
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<VAR>hg₂1 : g₂ ≠ 1<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<VAR>hg₂1 : g₂ ≠ 1<VAR>hg₁r : g₁ ∉ (φ i).range<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<VAR>hg₂1 : g₂ ≠ 1<VAR>hg₁r : g₁ ∉ (φ i).range<VAR>hg₂r : g₂ ∉ (φ j).range<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<VAR>hg₂1 : g₂ ≠ 1<VAR>hg₁r : g₁ ∉ (φ i).range<VAR>hg₂r : g₂ ∉ (φ j).range<VAR>w : Word G := { toList := [⟨i, g₁⟩, ⟨j, g₂⁻¹⟩], ne_one := ⋯, chain_ne := ⋯ }<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<VAR>hg₂1 : g₂ ≠ 1<VAR>hg₁r : g₁ ∉ (φ i).range<VAR>hg₂r : g₂ ∉ (φ j).range<VAR>w : Word G := { toList := [⟨i, g₁⟩, ⟨j, g₂⁻¹⟩], ne_one := ⋯, chain_ne := ⋯ }<VAR>hw : Reduced φ w<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : PushoutI φ<VAR>g₁ : G i<VAR>hg₁ : (of i) g₁ = x<VAR>g₂ : G j<VAR>hg₂ : (of j) g₂ = x<VAR>hx : ¬x ∈ (base φ).range<VAR>hx1 : x ≠ 1<VAR>hg₁1 : g₁ ≠ 1<VAR>hg₂1 : g₂ ≠ 1<VAR>hg₁r : g₁ ∉ (φ i).range<VAR>hg₂r : g₂ ∉ (φ j).range<VAR>w : Word G := { toList := [⟨i, g₁⟩, ⟨j, g₂⁻¹⟩], ne_one := ⋯, chain_ne := ⋯ }<VAR>hw : Reduced φ w<VAR>this : w = Word.empty<GOAL>False
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>(base φ).range ≤ (of i).range
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>((of i).comp (φ i)).range ≤ (of i).range
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : H<GOAL>((of i).comp (φ i)) h ∈ (of i).range
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>(base φ).range ≤ (of j).range
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>((of j).comp (φ j)).range ≤ (of j).range
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : H<GOAL>((of j).comp (φ j)) h ∈ (of j).range
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝⁴ : DecidableRel G.Adj<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : NonAssocSemiring α<VAR>i j : V<GOAL>(1 + adjMatrix α G + fun i j => if i = j then 0 else if adjMatrix α G i j = 0 then 1 else 0) i j = of (fun x x => 1) i j
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝⁴ : DecidableRel G.Adj<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : NonAssocSemiring α<VAR>i j : V<GOAL>(((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) + if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) = 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>count a (b :: l) = count a l + if a = b then 1 else 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>K : Submodule R M<VAR>x✝ : M₂<GOAL>x✝ ∈ map (↑e) K ↔ x✝ ∈ comap (↑e.symm) K
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>h_comm : Commute x y<VAR>hx : IsNilpotent x<VAR>hy : IsNilpotent y<GOAL>IsNilpotent (x - y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>h_comm : Commute x (-y)<VAR>hx : IsNilpotent x<VAR>hy : IsNilpotent y<GOAL>IsNilpotent (x - y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>h_comm : Commute x (-y)<VAR>hx : IsNilpotent x<VAR>hy : IsNilpotent (-y)<GOAL>IsNilpotent (x - y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>h_comm : Commute x (-y)<VAR>hx : IsNilpotent x<VAR>hy : IsNilpotent (-y)<GOAL>IsNilpotent (x + -y)
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : OreSet R⁰<VAR>inst✝ : NoZeroDivisors R<VAR>r : R<VAR>s : ↥R⁰<VAR>h : r /ₒ s ≠ 0<GOAL>r /ₒ s * (r /ₒ s)⁻¹ = 1
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : OreSet R⁰<VAR>inst✝ : NoZeroDivisors R<VAR>r : R<VAR>s : ↥R⁰<VAR>h : r /ₒ s ≠ 0<GOAL>(r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : OreSet R⁰<VAR>inst✝ : NoZeroDivisors R<VAR>r : R<VAR>s : ↥R⁰<VAR>h : r /ₒ s ≠ 0<VAR>hr : r ≠ 0<GOAL>(r /ₒ s * if h : False then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<GOAL>‖x‖ = ↑(max (x 0).natAbs (x 1).natAbs)
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<GOAL>‖x‖₊ = max ↑(x 0).natAbs ↑(x 1).natAbs
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>c : NNReal<GOAL>‖x‖₊ ≤ c ↔ max ↑(x 0).natAbs ↑(x 1).natAbs ≤ c
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<GOAL>∃ N, lift.{max u v w, w} κ ≤ #↑N
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<GOAL>∃ N, lift.{max u v w, w} κ ≤ #↑N
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<GOAL>lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<VAR>this : ↑N ⊨ L.distinctConstantsTheory Set.univ<GOAL>lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<VAR>this : ↑N ⊨ L.distinctConstantsTheory Set.univ<GOAL>lift.{max u v w, w} κ ≤ #↑N
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<VAR>this : ↑N ⊨ L.distinctConstantsTheory Set.univ<GOAL>lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #↑N
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<VAR>this : ↑N ⊨ L.distinctConstantsTheory Set.univ<GOAL>lift.{max (max u v) w, w} #↑Set.univ ≤ #↑N
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>κ : Cardinal.{w}<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : M ⊨ T<VAR>inst✝ : Infinite M<VAR>N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType<VAR>this : ↑N ⊨ L.distinctConstantsTheory Set.univ<GOAL>lift.{max u v w, max (max u v) w} (lift.{w, max (max u v) w} #↑N) ≤ lift.{max u v w, max (max u v) w} #↑N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>(Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal).IsPrime
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n j : ℕ<VAR>ij : i < j + 1<VAR>jn : j + 1 < n<GOAL>xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n j : ℕ<VAR>ij : i < j + 1<VAR>jn : j + 1 < n<GOAL>xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n j : ℕ<VAR>ij : i < j + 1<VAR>jn : j + 1 < n<GOAL>xn a1 j < xn a1 (j + 1)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁵ : CommRing R₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i✝ : ι<VAR>j✝ : ι'<VAR>N : Type u_9<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>ι'' : Type u_10<VAR>inst✝ : Fintype ι'<VAR>b'' : ι'' → M<VAR>this✝¹ : DecidableEq ι<VAR>this✝ : DecidableEq ι'<VAR>this : DecidableEq ι''<VAR>i : ι<VAR>j : ι''<GOAL>(b.toMatrix ⇑b' * b'.toMatrix b'') i j = b.toMatrix b'' i j
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompactSpace α<VAR>f : α →ᵇ β<VAR>M : ℝ<GOAL>‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompactSpace α<VAR>f : α →ᵇ β<VAR>M : ℝ<GOAL>dist f 0 < M ↔ ∀ (x : α), dist (f x) 0 < M
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u : Set α<VAR>hab : a ≠ b<VAR>s : Set α<GOAL>insert a (s \ {b}) = insert a s \ {b}